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.