Provable elimination of information leakage through timing channels

该项目旨在开发技术，以解决由于竞争共享硬件资源而导致的未经授权的信息流的信息安全问题。该项目将结合操作系统设计、形式化硬件模型、信息流推理和定理证明来实现一个被广泛认为不可行的目标。该项目预计将产生一个系统，防止通过定时通道泄露关键信息，如加密密钥。这应该可以防止针对公共云、移动设备和军用级别跨域设备的复杂攻击。

This project aims to develop techniques to solve the issue in information security of unauthorised information flow resulting from competition for shared hardware resources. The project will combine operating systems design, formal hardware models, information-flow reasoning and theorem proving to achieve a goal that is widely considered infeasible. The project is expected to result in a system that prevents leakage of critical information, such as encryption keys, through timing channels. This should prevent sophisticated attacks on public clouds, mobile devices and military-grade cross-domain devices.