| NSF Org: |
CNS Division Of Computer and Network Systems |
| Recipient: |
|
| Initial Amendment Date: | July 20, 2017 |
| Latest Amendment Date: | June 11, 2022 |
| Award Number: | 1718713 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Sol Greenspan
sgreensp@nsf.gov (703)292-7841 CNS Division Of Computer and Network Systems CSE Direct For Computer & Info Scie & Enginr |
| Start Date: | August 1, 2017 |
| End Date: | July 31, 2023 (Estimated) |
| Total Intended Award Amount: | $451,931.00 |
| Total Awarded Amount to Date: | $451,931.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
ONE CASTLE POINT ON HUDSON HOBOKEN NJ US 07030-5906 (201)216-8762 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
NJ US 07030-5991 |
| 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
The project investigates how flows of information through cybersystems can be accurately detected, controlled, and explained. Methods from programming languages and mathematical logic are being extended to enable the analysis of information flow, that is, to address data confidentiality and integrity requirements that must be met to achieve security and privacy goals. These analyses are the basis for making systems transparent in the sense that stakeholders will be able to see and understand the flows of information in cyberspace. The research has the potential to transform computing practice by ensuring accountability of system designers and builders through evidence that includes mathematically precise specifications and proofs. By advancing the science of security, and bringing that science into K-12 education, this project is helping to broaden society's understanding of computational thinking to include principle-based models of security and privacy. This in turn will reduce security risks due to user behaviors, and increase the adoption of beneficial IT systems while protecting individual privacy.
By formulating inference and verification problems in terms of relational logic, wherein pairs of programs and program executions are compared, the research addresses core problems such as translating programs in high level domain-specific languages into lower level language with good performance and without risk of security vulnerabilities and privacy violations. Another problem addressed is correctness by construction, through instrumentation that monitors information flow within and across abstraction layers. This research is helping to make it possible for cybersystems to be designed and evaluated on the basis of evidence including formal specification and proof for end-to-end requirements, resting on machine-checked formal proofs of system components and their compositions. The project is making possible programming frameworks that enable building security in, and enabling tool developers and security analysts to more quickly address new concerns -- threats, platforms, languages -- with benefit of reusable modular theories and techniques.
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.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
The aim of this project was to investigate how flows of information through cybersystems can be detected, controlled, and explained. The ultimate goal is to make it possible for cybersystems to be designed and evaluated on the basis of evidence including formal specifications of end-to-end security and privacy requirements, resting on formal proofs of system components and their compositions. The research supports programming frameworks that enable tool developers and security analysts to quickly address new concerns -- threats, platforms, languages -- with benefit of reusable modular theories and techniques.
Intellectual merit:
The primary technical focus of the project is relational program logics, which are deductive systems for proving properties that involve two program executions. One such property is behavioral equivalence between two programs, for example between an improved program and its predecessor, or between a source program and a version that has been hardened with security mechanisms. Another two-execution property, nonintereference, the basis to specify confidentiality and integrity requirements.
One major outcome is a deductive system, relational region logic (RelRL), its formal validation with respect to program semantics, and its experimental validation using a prototype tool based on the logic. RelRL advances the state of the art by effectively handling pointer-based dynamically allocated data structures, which are pervasive in practice and which pose challenges for formalization. Using RelRL, researchers settled an open problem dating from 1972: proofs of equivalence of data representations for pointer programs. Data abstraction is essential for modular software development. Evaluations of RelRL demonstrated its effectiveness on representative programs beyond the scope of state of the art automated reasoning systems. A key feature of RelRL supports reasoning by "aligning" related subprograms.
From prior work it was known that, for successful relational verification, good alignment is crucial. The standard notion of logical completeness failed to account for this. One project outcome is a new theory called alignment completeness which is applicable to any relational logic and which shed light on the limitations of prior work. One finding of the project is that for alignment completeness, a relational logic should include means to rewrite program control structure. The well established algebraic theory of control structure called Kleene Algebra with Tests (KAT) serves this purpose well.
Another outcome of this project is the development of an algebraic theory, BiKAT, which extends KAT to explicit reasoning about alignment. Its development led to discovery of proof rules for "forall-exists properties" that capture security and other requirements for nondeterministic programs. This in turn led to development of a new deductive system that is alignment complete for such properties. It also led to development of a complete automata-based method for proving such properties.
High level system security requirements may best be formulated in terms of knowledge: what can an adversary learn from observing the system. Mathematically, knowledge is a so-called hyperproperty, formulated in terms of multiple system executions. One outcome of this project formulates knowledge-based security properties in a way that accounts for confidentiality policies that allow downgrading of sensitive information under specific conditions. This formulation serves as basis for enforcement by means of runtime monitoring as well as statically by modular verification using relational logics. This approach has been realized in a verification tool for C programs that has been used to prove security of programs including a sealed-bid auction server and a differentially-private location service.
Tools based on deductive logics require verification expertise on the part of their users. Type systems are within the expertise of ordinary software developers, and basic confidentiality policies can be enforced on source programs by means of special-purpose type systems. One outcome of this project is a way to encode security policy using a standard type system that supports data abstraction, and to establish the security guaranteed by this encoding based on the existing data abstraction property.
Broader impact:
This research advanced the science needed for static and dynamic techniques for achieving strong assurance of information flow security. The ultimate impact will be improved security and privacy for software systems.
These outcomes are documented in a number of peer-reviewed publications. Publically available artifacts from the project include prototype tools for relational verification, a malloc/free system verified using the Verified Software Toolchain, and several verification case studies.
The award supported research training for a post-doctoral researcher, two PhD students, and several undergraduates. Drawing on results from the project, the PI developed a new course on Formal Verification of Hyperproperties.
Last Modified: 11/29/2023
Modified by: David A Naumann
Please report errors in award information by writing to: awardsearch@nsf.gov.
