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

点击翻译按钮获取中文摘要

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.