Date: Thursday 30 March 2017
Time: 16:00 - 17:30
Location / Room: 2BC

Chair:
Francesco Regazzoni, AlaRI/USI, CH

Co-Chair:
Georg Sigl, TU Munich, DE

Security tools provide support to build secure systems. Such techniques have made great progress in past years with improvements in SAT solvers, theorem provers and available computing power. This session includes papers that perform information flow checks on hardware designs, to check for information leaks either directly through analysis of the design or indirectly through timing channels.

Time	Label	Presentation Title Authors
16:00	12.3.1	REGISTER TRANSFER LEVEL INFORMATION FLOW TRACKING FOR PROVABLY SECURE HARDWARE DESIGN Speaker: Ryan Kastner, University of California, San Diego, US Authors: Armaiti Ardeshiricham1, Wei Hu2, Joshua Marxen2 and Ryan Kastner3 1University of California San Diego, US; 2University of California, San Diego, US; 3UCSD, US Abstract Information Flow Tracking (IFT) provides a formal methodology for modeling and reasoning about security properties related to integrity, confidentiality, and logical side channel. Recently, IFT has been employed for secure hardware design and verification. However, existing hardware IFT techniques either require designers to rewrite their hardware specifications in a new language or do not scale to large designs due to a low level of abstraction. In this work, we propose Register Transfer Level IFT (RTLIFT), which enables verification of security properties in an early design phase, at a higher level of abstraction, and directly on RTL code. The proposed method enables a precise understanding of all logical flows through RTL design and allows various tradeoffs in IFT precision. We show that RTLIFT achieves over 5x speedup in verification performance as compared to gate level IFT while minimizing the required effort for the designer to verify security properties on RTL designs. Download Paper (PDF; Only available from the DATE venue WiFi)
16:30	12.3.2	DUDE, IS MY CODE CONSTANT TIME? Speaker: Oscar Reparaz, KU Leuven/COSIC, BE Authors: Oscar Reparaz1, Josep Balasch1 and Ingrid Verbauwhede2 1Katholieke Universiteit Leuven, BE; 2KU Leuven - COSIC, BE Abstract This paper introduces dudect: a tool to assess whether a piece of code runs in constant time or not on a given platform. We base our approach on leakage detection techniques, resulting in a very compact, easy to use and easy to maintain tool. Our methodology fits in around 300 lines of C and runs on the target platform. The approach is substantially different from previous solutions. Contrary to others, our solution requires no modeling of hardware behavior. Our solution can be used in black-box testing, yet benefits from implementation details if available. We show the effectiveness of our approach by detecting several variable-time cryptographic implementations. We place a prototype implementation of dudect in the public domain. Download Paper (PDF; Only available from the DATE venue WiFi)
17:00	12.3.3	INFORMATION FLOW TRACKING IN ANALOG/MIXED-SIGNAL DESIGNS THROUGH PROOF-CARRYING HARDWARE IP Speaker: Yiorgos Makris, The University of Texas at Dallas, US Authors: Mohammad-Mahdi Bidmeshki, Angelos Antonopoulos and Yiorgos Makris, The University of Texas at Dallas, US Abstract Information flow tracking (IFT) is a widely used methodology for ensuring data confidentiality in electronic systems and numerous such methods have been developed at various software or hardware description levels. Among them, proof-carrying hardware intellectual property (PCHIP) introduced an IFT methodology for digital hardware designs described in hardware description languages (HDLs). The risk of accidental information leakage, however, is not restricted to the digital domain. Indeed, analog signals originating from sources of sensitive information, such as biometric sensors, as well as analog outputs of a circuit, could carry or leak secrets, respectively. Moreover, similar to digital designs, analog circuits can also be contaminated with malicious information leakage channels capable of evading traditional manufacturing test. Compounding the problem, in analog/mixed-signal circuits such information leakage channels can cross the analog/digital or digital/analog interface, making their detection even harder. To this end, in this paper we introduce a PCHIP-based methodology which enables systematic formal evaluation of information flow policies in analog/mixed-signal designs. As we demonstrate, by integrating information flow tracking across the digital and analog domain, our method is able to detect sensitive data leakage from the digital domain to the analog domain and vice versa, without requiring any modification of the current analog/mixed-signal circuit design flow. Download Paper (PDF; Only available from the DATE venue WiFi)
17:30		End of session