Secure information flow verification with mutable dependent types
Secure information flow verification with mutable dependent types
复制标题
使用可变依赖类型进行安全信息流验证
DOI：
10.1145/3061639.3062316
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
G. Suh
中科院分区：
文献类型：
--
作者：
Andrew Ferraiuolo;Weizhe Hua;A. Myers;G. Suh
本文提出了一种新的安全硬件描述语言（HDL），使用信息流类型的系统，以确保硬件是安全的设计时间。这种HDL的新奇在于它能够在多个安全级别上安全地共享硬件模块和存储元素。与以前的安全HDL不同，新的HDL以精细的粒度实现安全共享，而无需隐式添加硬件来执行安全性;这一点很重要，因为隐式添加的硬件可能会破坏功能并损害效率。新的HDL实现了安全、正确和高效的实用硬件设计。我们证明了新的HDL的实用性，通过使用它来设计和类型检查一个可合成的流水线处理器实现，支持保护环和指令，改变模式。
This paper presents a novel secure hardware description language (HDL) that uses an information flow type system to ensure that hardware is secure at design time. The novelty of this HDL lies in its ability to securely share hardware modules and storage elements across multiple security levels. Unlike previous secure HDLs, the new HDL enables secure sharing at a fine granularity and without implicitly adding hardware for security enforcement; this is important because the implicitly added hardware can break functionality and harm efficiency. The new HDL enables practical hardware designs that are secure, correct, and efficient. We demonstrate the practicality of the new HDL by using it to design and type-check a synthesizable pipelined processor implementation that support protection rings and instructions that change modes.