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

该项目研究如何准确地检测、控制和解释通过网络系统的信息流。来自编程语言和数理逻辑的方法正在得到扩展，以便能够分析信息流，即解决实现安全和隐私目标所必须满足的数据机密性和完整性要求。这些分析是使系统变得透明的基础，因为利益攸关方将能够看到和理解网络空间中的信息流动。这项研究有可能通过包括精确的数学规范和证明的证据来确保系统设计者和建造者的责任，从而改变计算实践。通过推进安全科学，并将该科学纳入K-12教育，该项目正在帮助扩大社会对计算思维的理解，将基于原则的安全和隐私模型包括在内。在保护个人隐私的同时，减少用户行为带来的安全风险，增加对有益IT系统的采用。通过从关系逻辑的角度制定推理和验证问题，将程序和程序执行对进行比较，解决了将高级领域特定语言的程序翻译成性能良好且没有安全漏洞和隐私侵犯风险的低级语言等核心问题。解决的另一个问题是通过构造的正确性，通过监视抽象层内和抽象层之间的信息流的插装。这项研究有助于在证据的基础上设计和评估网络系统，这些证据包括端到端需求的正式规范和证明，以及系统组件及其组成的机器检查的正式证明。该项目正在使能够构建安全性的编程框架成为可能，并使工具开发人员和安全分析人员能够更快地解决新的问题--威胁、平台、语言--并受益于可重复使用的模块化理论和技术。

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.