A High-Assurance, High-Performance Hardware-Based Cross-Domain System.
SAFECOMP(2016)
摘要
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.
更多查看译文
关键词
Cross-domain System, Regular Expressions, Domain-specific Language, Higher-order Logic, Logical Guard
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络