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

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

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.