Proving Flow Security of Sequential Logic via Automatically-Synthesized Relational Invariants
Proving Flow Security of Sequential Logic via Automatically-Synthesized Relational Invariants
复制标题
DOI：
10.1109/csf.2017.35
复制
发表时间：
2017-08
期刊：
影响因子：
--
通讯作者：
Hyoukjun Kwon;William R. Harris;H. Esmaeilzadeh
中科院分区：
文献类型：
--
作者：
Hyoukjun Kwon;William R. Harris;H. Esmaeilzadeh
Due to the proliferation of reprogrammable hardware, core designs built from modules drawn from a variety of sources execute with direct access to critical system resources. Expressing guarantees that such modules satisfy, in particular the dynamic conditions under which they release information about their unbounded streams of inputs, and automatically proving that they satisfy such guarantees, is an open and critical problem.,,To address these challenges, we propose a domain-specific language, named STREAMS, for expressing information-flow policies with declassification over unbounded input streams. We also introduce a novel algorithm, named SIMAREL, that given a core design C and STREAMS policy P, automatically proves or falsifies that C satisfies P. The key technical insight behind the design of SIMAREL is a novel algorithm for efficiently synthesizing relational invariants over pairs of circuit executions.,,We expressed expected behavior of cores designed independently for research and production as STREAMS policies and used SIMAREL to check if each core satisfies its policy. SIMAREL proved that half of the cores satisfied expected behavior, but found unexpected information leaks in six open-source designs: an Ethernet controller, a flash memory controller, an SD-card storage manager, a robotics controller, a digital-signal processing (DSP) module, and a debugging interface.
