TC: Large: Collaborative Research: Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software

该奖项是根据2009年《美国复苏和再投资法案》(公法111-5)提供资金的。该研究致力于将基础形式化方法和轻量级形式化方法相结合来验证大型软件系统的安全性、安全性和可靠性。基本方法(形式化方法)强调表现力和概括性，但它们还没有成功地扩展到大规模系统。轻量级方法强调自动化和可伸缩性，但它们在低级程序和提供明确的证据方面效率较低。PIS正在开发新的高级别和低级别轻量级方法，并将其应用于各种基础验证系统。更具体地说，在高层，PI正在开发轻量级依赖类型系统和分离逻辑形状分析，并连接传统类型系统、切片分析和流分析等当前方法；在低层，PI正在设计专门的验证器和决策程序，以验证低级别程序并支持异类组件的认证链接。如果成功，该研究将极大地提高基础验证系统的可扩展性，并为构建可信软件系统提供新的强大技术。结合轻量级和基础性方法还提供了一条共同的主线，将不同的验证社区联系在一起，并将它们统一到一个单一的框架中。

This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5). This research focuses on combining foundational and lightweight formal methods to verify the safety, security, and dependability of large-scale software systems. Foundational approaches (to formal methods) emphasize expressiveness and generality, but they have not been successfully scaled to large-scale systems. Lightweight approaches emphasize automation and scalability, but they are less effective on low-level programs and on providing explicit proof witness. The PIs are developing new high-level and low-level lightweight methods and adapting them into various foundational verification systems. More specifically, at the high level, the PIs are developing lightweight dependent-type systems and separation-logic shape analysis, and connecting current methods such as conventional type systems, slicing analysis, and flow analysis; at the low level, the PIs are designing specialized provers and decision procedures to verify low-level programs and to support certified linking of heterogeneous components. If successful, this research will dramatically improve the scalability of foundational verification systems and provide new powerful technologies for building trustworthy software systems. Combining lightweight and foundational approaches also provides a common thread that will pull different verification communities together and unify them into a single framework.