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

SaTC：核心：小型：信息保障和隐私的关系验证

• 批准号: 1718713
• 负责人: David Naumann
• 金额: $ 45.19万
• 依托单位: Stevens Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-08-01 至 2023-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1718713&HistoricalAwards=false
• 关键词: SaTC; CORE; Small; Relational; Verification

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.

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

项目成果

Toward Tool-Independent Summaries for Symbolic Execution

走向独立于工具的符号执行摘要

• 发表时间: 2023
• 期刊: ECOOP
• 作者: Ramos, Frederico;Sabino, Nuno;Adão, Pedro;Naumann, David A.;Fragoso Santos, José
• 通讯作者: Fragoso Santos, José

An illustrated guide to the model theory of supertype abstraction and behavioral subtyping

超类型抽象和行为子类型化模型理论的图解指南

• 发表时间: 2018
• 期刊: Engineering Trustworthy Software Systems
• 作者: Leavens, Gary T;Naumann, David A
• 通讯作者: Naumann, David A

The WhyRel Prototype for Modular Relational Verification of Pointer Programs

用于指针程序模块化关系验证的 WhyRel 原型

• 发表时间: 2023
• 期刊: Springer
• 作者: Nagasamudram, Ramana;Banerjee, Anindya;Naumann, David A
• 通讯作者: Naumann, David A

Thirty-seven years of relational Hoare logic: remarks on its principles and history

关系霍尔逻辑三十七年：对其原理和历史的评论

• 发表时间: 2020
• 期刊: Verification and Validation
• 作者: Naumann, David A

Assuming you know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies

假设您知道：表达流策略的关系注释的认知语义

• 发表时间: 2018
• 期刊: IEEE Computer Security Foundations Symposium
• 作者: Chudnov, Andrey;Naumann, David
• 通讯作者: Naumann, David