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.