Advertisement

A High-Assurance, High-Performance Hardware-Based Cross-Domain System

  • David HardinEmail author
  • Konrad Slind
  • Mark Bortz
  • James Potts
  • Scott Owens
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9922)

Abstract

Guardol is a domain-specific language focused on the creation of high-assurance cross-domain systems (i.e., network guards). The Guardol system generates executable code from Guardol programs while also providing formal property specification and automated verification support. Guardol programs and specifications are translated to higher order logic, then deductively transformed to a form suitable for code generation. Recently, we extended Guardol to support regular expressions; this has enabled the creation of a class of fast and secure hardware guards. We justify the regular expression extension via proof that the extension compiles to the original language while preserving key correctness properties. In this paper, we detail the verified compilation of regular expression guards written in Guardol, producing Ada, Java, ML, and VHDL. We have compiled a regular expression guard written in Guardol to VHDL, then synthesized and tested the guard on a low-SWAP (Size, Weight, And Power) embedded FPGA-based hardware guard platform; performance of the FPGA guard core exceeded the data payload rate for UDP/IP packets on Gigabit Ethernet, while consuming less than 1 % of FPGA resources.

References

  1. 1.
    Ada Working Group (ISO WG 9). Ada Reference Manual: Language and Standard Libraries (2012)Google Scholar
  2. 2.
    Appel, A.W.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)CrossRefzbMATHGoogle Scholar
  3. 3.
    Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Boston (2003)Google Scholar
  4. 4.
    Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Proceedings of the 4th Workshop on Scala, SCALA 2013, New York, NY, USA, pp. 1:1–1:10. ACM (2013)Google Scholar
  5. 5.
    Bortz, M., Wilding, M., Marek, J., Hardin, D., Hiratzka, T.D., Limondin, P.: High-assurance architecture for routing of information between networks of differing security level. United States Patent 8,161,529, April 2012Google Scholar
  6. 6.
    Brzozowski, J.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Eysholdt, M., Behrens, H.: Xtext: implement your language faster than the quick and dirty way. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications Companion, SPLASH 2010, pp. 307–309. ACM (2010)Google Scholar
  8. 8.
    Gill, A., Bull, T., Kimmell, G., Perrins, E., Komp, E., Werling, B.: Introducing Kansas Lava. In: Scholz, S.-B., Morazán, M.T. (eds.) IFL 2009. LNCS, vol. 6041, pp. 18–35. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  9. 9.
    Greve, D., Slind, K.: A step-indexing approach to partial functions. In: Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications. Electronic Proceedings in Theoretical Computer Science, vol. 114, pp. 42–53 (2013)Google Scholar
  10. 10.
    Hardin, D., Slind, K., Whalen, M., Pham, T.H.: The Guardol language and verification system. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 18–32. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  11. 11.
    Institute of Electrical and Electronics Engineers: IEEE Standard VHDL Language Reference Manual (2000)Google Scholar
  12. 12.
    Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Texts and Monographs in Computer Science. Kluwer Academic, Boston (2000)Google Scholar
  13. 13.
    Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL 2014: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191. ACM Press, January 2014Google Scholar
  14. 14.
    Leino, K. Rustan M.: Developing verified programs with Dafny. In: Proceedings of the International Conference on Software Engineering, ICSE 2013, Piscataway, NJ, USA, pp. 1488–1490. IEEE Press (2013)Google Scholar
  15. 15.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  16. 16.
    Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press, Cambridge (1997)Google Scholar
  17. 17.
    Owens, S., Reppy, J., Turon, A.: Regular-expression derivatives re-examined. J. Funct. Program. 19(2), 173–190 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Parr, T., Fisher, K.: LL(*): the foundation of the ANTLR parser generator. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 425–436 (2011)Google Scholar
  19. 19.
    Pham, T.H., Gacek, A., Whalen, M.W.: Reasoning about algebraic data types with abstractions. J. Autom. Reasoning (2016, to appear)Google Scholar
  20. 20.
    Rockwell Collins: Rockwell Collins Turnstile Selected for UCDMO’s Baseline List of Validated Cross Domain Products, March 2012Google Scholar
  21. 21.
    Slind, K., Hardin, D., Davis, J., Owens, S.: Benefits of using logic as an intermediate verification language. In: Review (2016)Google Scholar
  22. 22.
    Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, New York, NY, USA, pp. 97–108, ACM (2007)Google Scholar
  24. 24.
    Wilding, M., Greve, D., Richards, R., Hardin, D.: Formal verification of partition management for the AAMP7G microprocessor. In: Hardin, D. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 175–192. Springer, New York (2010)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • David Hardin
    • 1
    Email author
  • Konrad Slind
    • 1
  • Mark Bortz
    • 1
  • James Potts
    • 1
  • Scott Owens
    • 2
  1. 1.Rockwell Collins Advanced Technology CenterCedar RapidsUSA
  2. 2.University of KentCanterburyUK

Personalised recommendations