SaTC: CORE: Small: Relational Verification for Information Assurance and Privacy

Project: Research project

Project Details

Description

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.

StatusFinished
Effective start/end date1/08/1731/07/23

Funding

  • National Science Foundation

Fingerprint

Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.