SMASHUP: a toolchain for unified verification of hardware/software co-designs

1. Allamigeon, X., Blanchet, B.: Reconstruction of attacks against cryptographic protocols. In: 18th IEEE Workshop on Computer Security Foundations, 2005 (CSFW-18, 2005) (2005)

2. Apvrille, L., Roudier, Y.: SysML-Sec: A SysML environment for the design and development of secure embedded systems. In: APCOSEC 2013 (2013)

3. Arias, O., Davi, L., Hanreich, M., Jin, Y., Koeberl, P., Paul, D., Sadeghi, A.R., Sullivan, D.: HAFIX: hardware-assisted flow integrity extension. In: 52nd Design Automation Conference (DAC) (2015)

4. Armstrong, R.C., Punnoose, R.J., Wong, M.H., Mayo, J.R.: Survey of existing tools for formal verification. Tech. rep., Sandia National Laboratories (2014)

5. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems (1999)

6. Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings 14th IEEE Computer Security Foundations Workshop, 2001 (2001)

7. Blanchet, B., Smyth, B., Cheval, V.: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. CNRS, Departement dInformatique, Ecole Normale Superieure, Paris (2015)

8. Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.: BAP: a binary analysis platform. In: Proceedings of the 23rd International Conference on Computer Aided Verification (2011)

9. Camurati, P., Prinetto, P.: Formal verification of hardware correctness: introduction and survey of current research. Computer 21(7), 8–19 (1988)

   Article  Google Scholar 

10. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification (2000)

11. Clarke, L.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2(3), 215–222 (1976)

    Article  MathSciNet  Google Scholar 

12. Clocksin, W., Mellish, C.S.: Programming in PROLOG. Springer, New York (2003)

    Book  MATH  Google Scholar 

13. Danger, J.L., Guilley, S., Porteboeuf, T., Praden, F., Timbert, M.: HCODE: hardware-enhanced real-time CFI. In: Proceedings of the 4th Program Protection and Reverse Engineering Workshop (2014)

14. Davidson, D., Moench, B., Ristenpart, T., Jha, S.: FIE on firmware: finding vulnerabilities in embedded systems using symbolic execution. In: Proceedings of the 22nd USENIX Security Symposium (USENIX Security 13) (2013)

15. Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983)

    Article  MathSciNet  MATH  Google Scholar 

16. D’Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(7), 1165–1178 (2008)

17. Dullien, T., Porst, S.: REIL: A Platform-Independent Intermediate Representation of Disassembled Code for Static Code Analysis (2009). http://www.zynamics.com/downloads/csw09.pdf

18. El Defrawy, K., Francillon, A., Perito, D., Tsudik, G.: SMART: secure and minimal architecture for (establishing a dynamic) root of trust. In: Proceedings of the Network and Distributed System Security Symposium (NDSS), San Diego (2012)

19. Fox, A., Myreen, M.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Interactive Theorem Proving (2010)

20. Hong, S., Oguntebi, T., Casper, J., Bronson, N., Kozyrakis, C., Olukotun, K.: A case of system-level hardware/software co-design and co-verification of a commodity multi-processor system with custom hardware. In: Proceedings of the Eighth IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis (2012)

21. Kern, C., Greenstreet, M.R.: Formal verification in hardware design: a survey. ACM Trans. Des. Autom. Electron. Syst. 4(2), 123–193 (1999)

    Article  Google Scholar 

22. Koeberl, P., Schulz, S., Sadeghi, A.R., Varadharajan, V.: TrustLite: a security architecture for tiny embedded devices. In: Proceedings of the Ninth European Conference on Computer Systems (2014)

23. Kroening, D., Sharygina, N.: Formal verification of systemC by automatic hardware/software partitioning. In: Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design (2005)

24. Noorman, J., Agten, P., Daniels, W., Strackx, R., Van Herrewege, A., Huygens, C., Preneel, B., Verbauwhede, I., Piessens, F.: Sancus: low-cost trustworthy extensible networked devices with a zero-software trusted computing base. In: Presented as part of the 22nd USENIX Security Symposium (USENIX Security 13) (2013)

25. Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th Colloquium on International Symposium on Programming (1982)

26. Schlich, B.: Model checking of software for microcontrollers. ACM Trans. Embed. Comput. Syst. 9(4), 36 (2010)

    Article  Google Scholar 

27. Schmidt, B., Villarraga, C., Fehmel, T., Bormann, J., Wedler, M., Nguyen, M., Stoffel, D., Kunz, W.: A new formal verification approach for hardware-dependent embedded system software. IPSJ Trans. Syst. LSI Des. Methodol. 6, 135–145 (2013)

    Article  Google Scholar 

28. Semeria, L., Ghosh, A.: Methodology for hardware/software co-verification in C/C++. In: Proceedings of the Asia and South Pacific Design Automation Conference, 2000 (ASP-DAC 2000) (2000)

29. Subramanyan, P., Arora, D.: Formal verification of taint-propagation security properties in a commercial SoC design. In: Design, Automation and Test in Europe Conference and Exhibition (DATE) (2014)

30. Villarraga, C., Schmidt, B., Bormann, J., Bartsch, C., Stoffel, D., Kunz, W.: An equivalence checker for hardware-dependent embedded system software. In: 2013 Eleventh IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE) (2013)

31. Villarraga, C., Schmidt, B., Bao, B., Raman, R., Bartsch, C., Fehmel, T., Stoffel, D., Kunz, W.: Software in a hardware view: new models for hw-dependent software in soc verification and test. In: 2014 International Test Conference (2014)

Download references