Stanford Engineering
Robust Systems Group (RSG)

Robust Operation: Bugs, Reliability, Security

Overview

Malfunctions of computing systems have serious consequences that continue to increase as systems become more complex, interconnected, and pervasive. Existing verification and test methods barely cope with today's system complexity. For coming generations of integrated circuits with remarkably small feature sizes, many reliability failure mechanisms (previously benign) are becoming critical. These barriers appear at a time when robust operation is essential more than ever, from self-driving cars all the way to cloud data centers.

Our current research focuses on design bugs and hardware security. Our past research has produced several key approaches to overcome reliability failures. Their adoption by industry is growing rapidly, in markets ranging from cloud computing to automotive systems. 

Hardware design bugs are inexorably increasing as designers resort to staggering complexity to meet system functionality, performance, and energy objectives. Design verification accounts for up to 80% of the overall design cost. A rising fraction of critical bugs frequently escape existing verification causing incorrect system operation, security risks, and expensive product delays and recalls.

Our new concepts, Quick Error Detection (QED) and Symbolic QED, overcome these significant challenges. With solid theoretical foundations, QED and Symbolic QED are producing dramatic results for industrial designs. An extensive study by Infineon Technologies concludes that Symbolic QED improves pre-silicon verification productivity 60-fold (from 9 person-months to 2 person-days) while detecting previously-undeteced bugs. Post-silicon validation studies by NXP (formerly Freescale) show similar dramatic benefits, from months using existing approaches to seconds using QED. 

QED-inspired techniques are also effective in detecting difficult hardware security vulnerabilities such as covert channel attacks (beyond Spectre, Meltdown) and hardware Trojans.

Related Publications

  1. F. Lonsing, S. Mitra and C. Barrett, “A Theoretical Framework for Symbolic Quick Error Detection,” Formal Methods in Computer-Aided Design, Sept. 2020.
  2. E. Singh, F. Lonsing, S. Chattopadhyay, M. Strange, P. Wei, X. Zhang, Y. Zhou, J. Cong, D. Chen, Z. Zhang, P. Raina, C. Barrett and S. Mitra, “A-QED Verification of Hardware Accelerators,” ACM/IEEE Design Automation Conf., San Francisco, CA, July 2020.
  3. M. Fadiheh, J. Muller, R. Brinkmann, S. Mitra, D. Stoffel and W. Kunz, “A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-order Processors,” ACM/IEEE Design Automation Conf., San Francisco, CA, July 2020.
  4. K. Devarajegowda, M. Fadiheh, E. Singh, C. Barrett, S. Mitra, W. Ecker, D. Stoffel and W. Kunz, “Gap-free Processor Verification by S²QED and Property Generation,” ACM/IEEE Design Automation and Test in Europe, Grenoble, France, March 2020.
  5. E. Singh, K. Devarajegowda, S. Simon, R. Schnieder, K. Ganesan, M. Fadiheh, D. Stoffel, W. Kunz, C. Barrett, W. Ecker and S. Mitra, “Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study,” IEEE/ACM Design Automation and Test in Europe, Florence, Italy, March 2019.
  6. M. Fadiheh, D. Stoffel, C. Barrett, S. Mitra and W. Kunz, “Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking,” IEEE/ACM Design Automation and Test in Europe, Florence, Italy, March 2019.
  7. E. Singh, D. Lin, C. Barrett and S. Mitra, “Logic Bug Detection and Localization using Symbolic Quick Error Detection,” IEEE Trans. CAD, May 2018.
  8. M. Fadiheh, J. Urdahl, S. Nuthakki, C. Barrett, S. Mitra, D. Stoffel and W. Kunz, “Symbolic Quick Error Detection with Symbolic Initial State for Pre-Silicon Verification,” ACM/IEEE Design Automation and Test in Europe, Dresden, Germany, March 2018.
  9. E. Singh, C. Barrett and S. Mitra, “E-QED: Electrical Bug Localization during Post-Silicon Validation Enabled by Quick Error Detection and Formal Methods,” Intl. Conf. Computer-Aided Verification, Heidelberg, Germany, July 2017.
  10. D. Lin, T. Hong, Y. Li, Eswaran S., S. Kumar, F. Fallah, N. Hakim, D.S. Gardner and S. Mitra, “Effective Post-Silicon Validation of System-on-Chips using Quick Error Detection,” IEEE Trans. CAD, Oct. 2014.