Project Details
Description
This NSF Cyber Trust project investigates techniques to achieve high assurance that systems satisfy information flow policies like confidentiality and integrity. Baseline policies are expressed by labeling component interfaces with security types, in accord with standard theory but extended to encompass role based trust management systems to deal with mutual distrust in distributed systems. The baseline policy is augmented more powerful methods. This is accomplished by designating certain procedures or subprograms as exempt from the baseline policy and instead subject to a specification in program logic (called ``flowspecs'') that expresses information downgrading. To check conformance with baseline policy, type checking is used. To check conformance with flowspecs, formal verification tools are used. Flowspecs are encoded in standard logic so that off the shelf tools can be used.
The broader impact is that confidentiality and integrity requirements must be expressed as such, with clear meaning for requirements analysts and implementers. Designs must explicitly account for the use of access controls and other means to satisfy information flow requirements. Designs and implementations must be checked for conformance with information flow policies, accounting for interaction with less trustworthy components. Rigorous validation tools must serve both to ensure compliance and also to help avoid waste of resources in unnecessary runtime checks, monitoring, or other security measures. Eventually, the tools must guide developers and facilitate system administration, so that trustworthiness is maintained as circumstances change and systems evolve. An immediate impact of the project is in training undergraduate and graduate students through research, coursework, and industry collaborations.
Status | Finished |
---|---|
Effective start/end date | 15/09/06 → 31/08/10 |
Funding
- National Science Foundation