More Like this

1. Uncovering Bugs in P4 Programs with Assertion-based Verification

   https://doi.org/10.1145/3185467.3185499  

   Freire, Lucas ; Neves, Miguel ; Leal, Lucas ; Levchenko, Kirill ; Schaeffer-Filho, Alberto ; Barcellos, Marinho ( March 2018 , Proceedings of the Symposium on SDN Research)

   Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. Existing data plane verification approaches are unable to model P4 programs, or they present severe restrictions in the set of properties that can be modeled. In this paper, we introduce a data plane program verification approach based on assertion checking and symbolic execution. Network programmers annotate P4 programs with assertions expressing general security and correctness properties. Once annotated, these programs are transformed into C-based models and all their possible paths are symbolically executed. Results show that the proposed approach, called ASSERT-P4, can uncover a broad range of bugs and software flaws. Furthermore, experimental evaluation shows that it takes less than a minute for verifying various P4 applications proposed in the literature. 

   more » « less
2. Automated Test Generation for Activation of Assertions in RTL Models

   https://doi.org/10.1109/ASP-DAC47756.2020.9045731  

   Lyu, Yangdi ; Mishra, Prabhat ( January 2020 , Asia and South Pacific Design Automation Conference (ASP-DAC))

   A major challenge in assertion-based validation is how to activate the assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results show that the directed tests are able to activate assertions non-vacuously. 

   more » « less
3. Directed Test Generation for Activation of Security Assertions in RTL Models

   https://doi.org/10.1145/3441297  

   Witharana, Hasini ; Lyu, Yangdi ; Mishra, Prabhat ( April 2021 , ACM Transactions on Design Automation of Electronic Systems)

   null (Ed.)

   Assertions are widely used for functional validation as well as coverage analysis for both software and hardware designs. Assertions enable runtime error detection as well as faster localization of errors. While there is a vast literature on both software and hardware assertions for monitoring functional scenarios, there is limited effort in utilizing assertions to monitor System-on-Chip (SoC) security vulnerabilities. We have identified common SoC security vulnerabilities and defined several classes of assertions to enable runtime checking of security vulnerabilities. A major challenge in assertion-based validation is how to activate the security assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results on diverse benchmarks demonstrate that the directed tests are able to activate security assertions non-vacuously. 

   more » « less
4. Automated Generation of Security Assertions for RTL Models

   https://doi.org/10.1145/3565801  

   Witharana, Hasini ; Jayasena, Aruna ; Whigham, Andrew ; Mishra, Prabhat ( January 2023 , ACM Journal on Emerging Technologies in Computing Systems)

   System-on-Chip (SoC) security is vital in designing trustworthy systems. Detecting and fixing a vulnerability in the early stages is easier and cost-effective. Assertion-based verification is widely used for functional validation of Register-Transfer Level (RTL) designs. Assertions can improve the controllability and observability that can lead to faster error detection and localization. Although assertions are widely used for functional validation of RTL models, there is limited effort in applying assertions to detect SoC security vulnerabilities. Specifically, a fundamental challenge in SoC security and trust validation is how to develop high-quality security assertions. In this article, we perform automated vulnerability analysis of RTL models to generate security assertions for six classes of vulnerabilities. Experimental results show that the generated security assertions can detect a wide variety of vulnerabilities. Our automated framework can drastically reduce the overall security validation effort compared to the manual development of security assertions. Automated generation of security assertions will enable assertion-based verification to be one of the most promising pre-silicon security sign-off solutions. 

   more » « less
5. Statistical assertions for validating patterns and finding bugs in quantum programs

   https://doi.org/10.1145/3307650.3322213  

   Huang, Yipeng ; Martonosi, Margaret ( June 2019 , Proceedings of the 46th International Symposium on Computer Architecture (ISCA ’19))

   In support of the growing interest in quantum computing experimentation, programmers need new tools to write quantum algorithms as program code. Compared to debugging classical programs, debugging quantum programs is difficult because programmers have limited ability to probe the internal states of quantum programs; those states are difficult to interpret even when observations exist; and programmers do not yet have guidelines for what to check for when building quantum programs. In this work, we present quantum program assertions based on statistical tests on classical observations. These allow programmers to decide if a quantum program state matches its expected value in one of classical, superposition, or entangled types of states. We extend an existing quantum programming language with the ability to specify quantum assertions, which our tool then checks in a quantum program simulator. We use these assertions to debug three benchmark quantum programs in factoring, search, and chemistry. We share what types of bugs are possible, and lay out a strategy for using quantum programming patterns to place assertions and prevent bugs. 

   more » « less