Visible to the public Proving Flow Security of Sequential Logic via Automatically-Synthesized Relational Invariants

TitleProving Flow Security of Sequential Logic via Automatically-Synthesized Relational Invariants
Publication TypeConference Paper
Year of Publication2017
AuthorsKwon, H., Harris, W., Esmaeilzadeh, H.
Conference Name2017 IEEE 30th Computer Security Foundations Symposium (CSF)
ISBN Number978-1-5386-3217-8
KeywordsAlgorithm design and analysis, automatically-synthesized relational invariants, circuit executions, core design C, debugging interface, declassification, digital signal processing chips, digital-signal processing module, domain-specific language, DSP module, dynamic conditions, Ethernet controller, field programmable gate arrays, flash memories, flash memory controller, flow security, Hardware, Hardware design languages, Human Behavior, human computer interaction, information leaks, information-flow policies, Local area networks, Named Data Network Security, open-source designs, pattern classification, program debugging, program verification, pubcrawl, Registers, resilience, Resiliency, robotics controller, Scalability, SD-card storage manager, security, security of data, sequential logic, SIMAREL, specification languages, storage management, STREAMS policies, unbounded input streams, user interfaces, Wires

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.

Citation Keykwon_proving_2017