ITR: Guarding Quasi-Invariants: Generalizing Specialization for System Software Security & Reliability

该项目将开发概念和技术，通过检测和管理代码中不可见的环节来提高系统软件的安全性和可靠性。不可见的链接是程序组件之间的依赖关系，很难通过单独查看代码来发现。不可见链接的一个常见来源是由于某些系统不变量而删除“不必要”代码的优化过程。软件的重用和发展可能会使这些不变量失效，破坏不可见的链接，并导致阿丽亚娜501火箭这样的崩溃。此外，诸如TOCTTOU（检查时间到使用时间）之类的恶意攻击经常利用不可见的链接。我们的方法结合了三种以前没有结合在一起的技术。首先是支持灵活的正确性标准定义的软件抽象，称为事务活动模型（Transactional Activity Model），它将标记包含不可见链接的代码边界。第二种是使用包装器在生产软件之上实现正确性标准的强制执行，例如，围绕Unix文件系统对TOCTTOU进行并发控制。第三，程序专门化技术，特别是准不变量的保护，可以使不可见的链接可见，并生成代码来维护这些链接的完整性（例如，确保文件没有被攻击者替换）。这种组合提供了揭示不可见链接的承诺，从而显式地管理这些依赖关系。

This project will develop concepts and techniques to improve the security and reliability of system software by detecting and managing invisible links in the code. Invisible links are dependencies among program components that are difficult to find by looking at the code alone. A common source of invisible links is the optimization process that removes "unnecessary" code due to some system invariants. Software reuse and evolution may invalidate these invariants, break invisible links, and cause crashes such as the Ariane 501 rocket. Further, malicious attacks such as TOCTTOU (time-of-check to time-of-use) often exploit invisible links. Our approach combines three techniques that have not been brought together previously. First is a software abstraction with support for flexible correctness criteria definitions, called Transactional Activity Model, which will demark code boundaries that contain invisible links. Second is the use of wrappers to implement the enforcement of correctness criteria on top of production software, for example, concurrency control around the Unix file system for TOCTTOU. Third, program specialization techniques, in particular, the guarding of quasi-invariants, can make invisible links visible and generate the code to maintain the integrity of these links (e.g., making sure the file has not been replaced by the attacker). This combination offers the promise to reveal invisible links and therefore manage those dependencies explicitly.