Collaborative Research: SaTC: CORE: Medium: End-to-end Verified Secure Sandboxed Systems

我们使用的几乎所有软件系统，从基于云的服务器应用程序到客户端Web浏览器，都是通过编写第三方代码构建的。不幸的是，这样的组合是不安全的，是无数野生袭击的来源。软件沙箱承诺限制第三方代码，并确保第三方代码中的错误不会危及整个系统。然而，现有的沙箱框架只考虑在沙箱中运行的代码，因此它们的安全保证不会扩展到大多数真正的程序，这些程序最终需要退出沙箱才能与外部世界通信。该项目将开发构建端到端安全沙箱系统的基础、技术和框架，这些系统即使跨越沙箱边界也能提供正式的安全保证。如果成功，这个项目将让开发人员安全地使用开源和第三方代码并从中受益，而不需要承担所有风险。这将反过来解决在构建大型软件系统时出现的许多安全问题以及与网络攻击相关的随之而来的经济和社会成本。调查人员将：(1)设计新型系统，允许开发人员显式编码沙箱边界不变量并自动生成通过构造而安全的边界代码；(2)开发沙箱上下文切换的正式基础，以表征安全上下文切换的机密性、完整性和可用性要求；以及(3)为沙箱运行时和暴露于沙箱程序以进行通信和执行I/O的关键操作系统抽象之间的接口开发形式化语义。这些形式基础将被用于合成验证安全的运行时系统和可移植系统接口，这将允许沙箱模块彼此、应用程序和操作系统服务安全地交互。该项目将在安全沙箱框架的设计、实现和验证方面产生新的创新，并产生新的技术和工具，使开发人员能够构建通过构建而安全的大规模系统。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Almost all software systems we use, from cloud-based server applications to client-side web browsers, are built by composing third-party code. Unfortunately, such composition is insecure and the source of countless attacks in the wild. Software sandboxing promises to confine third-party code and ensure that bugs in third-party code cannot compromise the whole system. However, existing sandboxing frameworks only reason about code running in the sandbox and thus their security guarantees don't extend to most real programs, which ultimately need to exit the sandbox to communicate with the outside world. This project will develop foundations, techniques, and frameworks for building end-to-end secure sandboxing systems that provide formal security guarantees even across the sandbox boundary. If successful, this project will let developers safely use and benefit from open source and third-party code, without needing to absorb all the risk. This will, in turn, address many of the security problems that arise when building large software systems and the ensuing financial and social costs associated with cyberattacks.The investigators will: (1) design novel type systems that will allow developers to explicitly encode sandbox boundary invariants and automatically generate boundary code that is secure by construction; (2) develop formal foundations for sandbox context-switching to characterize the confidentiality, integrity, and availability requirements of secure context-switching; and (3) develop a formal semantics for the interface between the sandbox runtime and the key operating system abstractions that are expose to sandboxed programs to communicate and perform I/O. Together, these formal foundations will be used to synthesize a verified-secure runtime system and portable system interface, which will allow sandboxed modules to safely interact with each other, the application, and operating system services. The project will yield new innovations in the design, implementation, and verification of secure sandboxing frameworks, and lead to new techniques and tools that will empower developers to build large-scale systems that are secure by construction.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.