- Home
- Research Areas
- Biological Sciences (BIO)
- Computer and Information Science and Engineering (CISE)
- Education and Human Resources (EHR)
- Engineering (ENG)
- Environmental Research and Education (ERE)
- Geosciences (GEO)
- Integrative Activities (OIA)
- International Science and Engineering (OISE)
- Mathematical and Physical Sciences (MPS)
- Social, Behavioral and Economic Sciences (SBE)
- Funding
- About Funding
- Archived Funding Search
- Due Dates
- Find Funding
- Merit Review
- Policies and Procedures
- Preparing Proposals
- Recent Opportunities
- Transformative Research
- Related Links
- Proposal and Award Policies and Procedures Guide (PAPPG)
- Research.gov
- FastLane
- Funding Opportunities For
- Graduate Students
- K-12 Educators
- Postdoctoral Fellows
- Undergraduate Students
- Small Business
- Awards
- Document Library
- News
- About NSF
Award Abstract # 1812522
SaTC: CORE: Small: verifying security for data non-interference
| NSF Org: |
CNS Division Of Computer and Network Systems |
| Awardee: |
|
| Initial Amendment Date: | August 10, 2018 |
| Latest Amendment Date: | August 10, 2018 |
| Award Number: | 1812522 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Phillip Regalia
pregalia@nsf.gov (703)292-2981 CNS Division Of Computer and Network Systems CSE Direct For Computer & Info Scie & Enginr |
| Start Date: | September 1, 2018 |
| End Date: | August 31, 2022 (Estimated) |
| Total Intended Award Amount: | $500,000.00 |
| Total Awarded Amount to Date: | $500,000.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Awardee Sponsored Research Office: |
77 MASSACHUSETTS AVE CAMBRIDGE MA US 02139-4301 (617)253-1000 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
MA US 02139-4307 |
| Primary Place of Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Secure &Trustworthy Cyberspace |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
Many security problems today stem from bugs in software. Although there has been significant effort in reducing bugs through better testing, fuzzing, model checking, and so on, subtle bugs remain and continue to be exploited. This proposal explores the use of formal verification to prove security of a file system implementation along with an example application in the form of a mail server. Machine-checked verification is a powerful approach that can eliminate a large class of bugs in software by proving that an implementation meets a precise specification. As long as the specification rules out a certain class of bugs, the machine-checked proof will ensure no such bugs can exist in the implementation. This project develops techniques for proving security of sophisticated applications, such as proving that a mail server will not inappropriately disclose confidential email messages. At the high level, the impact of this work will be a more secure software infrastructure.
The key technical challenge that this project focuses on is data confidentiality. The project explores approaches for specifying confidentiality of systems software, including a mail server and a POSIX file system, as well as a framework for implementation and machine-checked verification of confidentiality properties for these applications. The project also develops common infrastructure that such applications depend on, including a formal security specification for a POSIX file system and verified implementations of a mail server and a file system with proofs of security, which will be useful to the broader community. Finally, part of the project involves developing course modules focused on machine-checked proofs of correctness and security for systems software.
This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from this site.
Ileri, Atalay and Chajed, Tej and Chlipala, Adam and Kaashoek, Frans and Zeldovich, Nickolai
"Proving confidentiality in a file system using DISKSEC"
Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI)
, 2018
Citation Details
Athalye, Anish and Belay, Adam and Kaashoek, M. Frans and Morris, Robert and Zeldovich, Nickolai
"Notary: a device for secure transaction approval"
Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP 2019)
, 2019
https://doi.org/10.1145/3341301.3359661
Citation Details
Please report errors in award information by writing to: awardsearch@nsf.gov.
