TWC: Medium: Language-Hardware Co-Design for Practical and Verifiable Information Flow Control

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

Current cloud computing platforms, mobile computing devices, and embedded devices all have the security weakness that they permit information flows that violate the confidentiality or integrity of information. This project explores an integrated approach in which software and hardware are co-designed with strong, comprehensive, verifiable security assurance. The goal is to develop a methodology for designing systems in which all forms of information flow are tracked, at both the hardware and software levels, and between these levels. This can have a significant impact on how computing systems are designed, and could make the next generation of computing devices and platforms inherently more secure.The project investigates a novel hardware description language, that allows information flow and timing channels to be soundly tracked at the hardware level, while permitting fine-grained sharing and reuse of hardware resources across multiple security levels. The practicality of this approach will be demonstrated on a high-performance microprocessor with verified-secure information flow which is designed as part of the project. The project explores novel techniques for identifying information flows that must be communicated between the software and hardware levels in order for the hardware to enforce security, and operating-system mechanisms for automatically virtualizing rich language-level security policies onto the more limited palette of security levels representable in hardware. The project uses rigorous verification of the new language-level and hardware-level techniques to demonstrate that applications and hardware developed according to the new methodology provably enforce secure information flow throughout the computing system.