Static Previrtualization
Abstract:
The modular design of software has contributed greatly to the ability of application developers to quickly write sophisticated applications; however, in most instances only a small fraction of the functionality of particular software components is needed. The unmistakable trend is for operating systems and libraries to grow over time This trend is not going to reverse any time soon because it represents a growth in economic value: by adding support for more hardware, and features to support more applications, the operating system grows its ecosystem, and therefore its value. However, this level of bloat in the software stack is inimical to security: there is ever more, and more complex, code to be analyzed to achieve any given degree of assurance for a system. While most systems are not constrained by the resource limits that they were in the past the prevalence of security vulnerabilities that rely on live resources, such as jump-to-libc and return-oriented programming, suggests that even dead-functionality in binaries and shared libraries can be dangerous.
Partial evaluation offers a principles approach to address all aspects of operating system growth. By specializing an operating system with respect to a given set of applications to run on a given hardware configuration, only those features essential for the particular applications being deployed on a particular set of machines need remain. Partial evaluation can trim device drivers and other kernel modules down to the exact minimum required to support the application on the given hardware. To address the problem of extraneous functionality, we propose static previrtualization, a static analysis and code specialization technique that uses partial evaluation.
We, together with several collaborators, have implemented a preliminary version of static previrtualization in a tool called Occam that combines techniques from partial evaluation and link-time-optimization to specialize the software stack and thereby reduce the functionality available to applications. Occam uses types as a compositional mechanism to address the independent specialization of libraries and describe code compatibility and transformations that can be statically reasoned about and applied to code.
Biographies:
Natarjan Shankar
Natarjan Shankar is a Staff Scientist at SRI, International. Dr. Shankar has a Ph.D. in Computer Science from the University of Texas at Austin. His interests are in the study of formal methods for the specification and verification of hardware and software systems, automated deduction, and computational logic. He is the co-developer of several leading verification tools including PVS and SAL. His recent research has focused on inference architectures, cyber-physical systems, probabilistic inference, natural language processing, and formal tool integration. His recent work includes the development of inference techniques, software and hardware verification methods, tool integration frameworks, and probabilistic reasoning. Dr. Shankar leads an international initiative on the scientific challenges of verified software.
Ashish Gehani
Dr. Ashish Gehani is a member of the Computer Science Laboratory at SRI, International. He obtained his B.S. (Honors) degree in Mathematics from the University of Chicago, and his M.S. and Ph.D. degrees in Computer Science from Duke University. Dr. Gehani has conducted research on data provenance, digital forensics, intrusion prevention, protecting sensor networks, multimedia security, and biological computation. He has published over thirty peer-reviewed research papers and served as a reviewer for over two dozen conferences and journals.
Slide presentation will be available for download May 2012.