VeriSketch: Synthesizing Secure Hardware Designs with Timing-Sensitive Information Flow Properties
VeriSketch: Synthesizing Secure Hardware Designs with Timing-Sensitive Information Flow Properties
复制标题
VeriSketch：综合安全硬件设计与时间敏感信息流属性
DOI：
10.1145/3319535.3354246
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Kastner, Ryan
中科院分区：
文献类型：
--
作者：
Ardeshiricham, Armaiti;Takashima, Yoshiki;Gao, Sicun;Kastner, Ryan
我们提出了VeriSketch，这是一个面向安全的程序综合框架，用于开发具有正式功能和安全规范保证的硬件设计。VeriSketch定义了一种合成语言，一种用于指定和推断对时间敏感的信息流属性的代码工具框架，并使用专门的基于约束的合成来生成执行规范的HDL码。我们通过安全关键硬件设计实例，包括高速缓存控制器、线程调度器和片上系统仲裁器，展示了VeriSketch的强大功能，并正式保证了安全特性，如不存在定时侧通道、保密性和隔离性。
We present VeriSketch, a security-oriented program synthesis framework for developing hardware designs with formal guarantee of functional and security specifications. VeriSketch defines a synthesis language, a code instrumentation framework for specifying and inferring timing-sensitive information flow properties, and uses specialized constraint-based synthesis for generating HDL code that enforces the specifications. We show the power of VeriSketch through security-critical hardware design examples, including cache controllers, thread schedulers, and system-on-chip arbiters, with formal guarantee of security properties such as absence of timing side-channels, confidentiality, and isolation.
登录
查看更多内容
FlexPRET：用于混合关键性系统的处理器平台
DOI：
10.1109/rtas.2014.6925994
发表时间：
2014
期刊：
2014 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS)
影响因子：
--
作者：
Michael Zimmer;David Broman;C. Shaver;Edward A. Lee
通讯作者：
Edward A. Lee
DOI：
--
发表时间：
2013
期刊：
Asilomar Conference on Signals, Systems and Computers
影响因子：
--
作者：
Andrew Becker;D. Novo;P. Ienne
通讯作者：
P. Ienne
用于 SoC 验证的统一指令级抽象的基于模板的参数化综合
DOI：
--
发表时间：
2018
影响因子：
2.9
作者：
P. Subramanyan;Bo;Y. Vizel;Aarti Gupta;S. Malik
通讯作者：
S. Malik
使用反例引导的抽象细化有效执行运行时策略
DOI：
--
发表时间：
2012
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
Matt Fredrikson;R. Joiner;S. Jha;T. Reps;Phillip A. Porras;Hassen Saïdi;V. Yegneswaran
通讯作者：
V. Yegneswaran
DOI：
10.1145/1866307.1866340
发表时间：
2010-10
期刊：
--
影响因子：
--
作者：
William R. Harris;S. Jha;T. Reps
通讯作者：
William R. Harris;S. Jha;T. Reps