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.