Computer systems are increasingly handling important information and responsible for controlling and protecting critical infrastructures; insuring that they behave in a secure manner is of the utmost importance. Information flow tracking is an important technique for determining the security of a computing system. It works by “labeling” important data and then automatically determining how it will move throughout the microelectronic circuit. This can be used to verify that the hardware and software are behaving in a correct manner, and eliminate costly security flaws.

We have been working on hardware information flow tracking for almost a decade, and we now finally decided it is time to increase the level of abstraction from gate level to register transfer level. Our recent paper at Design, Automation and Test in Europe (DATE) — the premier conference for electronic system design and test — detailed the benefits this approach by showing that formal verification can be made substantially faster, and we can more easily provide tradeoffs between complexity (i.e., verification time) and accuracy. This allows us verify the security of larger circuits which is important as security rightfully becomes a more prevalent consider in the hardware design flow.

The paper “Register Transfer Level Information Flow Tracking for Provably Secure Hardware Design” was authored by Armaiti Ardeshiricham, Wei Hu, Joshua Marxen and Ryan Kastner. Ryan returned to Lausanne, Switzerland to give the talk. It was a beautiful week as evidenced by the picture taken in vineyards in nearby Epesses above Lake Geneva.