Hacker-Proof Code Confirmed

Re:Hacker-Proof Code Confirmed by fmap on Wednesday September 21, 2016 @05:52AM (#12546718)

This is very interesting work! Do you have axiomatic semantics for Ivory and Tower, and/or specifications for SMACCMPilot? If so, it might be interesting to show specification preservation from Ivory to the Verified Software Toolchain (I'm just assuming that Ivory targets some C subset compatible with Verifiable C). With the ARM backend of CompCert this would give high assurance right down to the machine code.

In any case, I found your experience report to be very well written and would love to hear more about this project.

[ Parent | on HN ]

Re:Hacker-Proof Code Confirmed by acfoltzer on Wednesday September 21, 2016 @09:07PM (#12553570)

Thanks for the kind words!

You might find our more recent Haskell Symposium paper of interest if you're interested in semantics (this is also a good reminder for us to update the webpage with a link): https://www.cs.indiana.edu/~lepike/pubs/ivory.pdf

Essentially, we built an Isabelle/HOL model of a Core Ivory language, and then used those semantics to prove type safety through the usual progress and preservation.

We don't have specifications of the higher-level properties of SMACCMPilot at the Ivory/Tower level. Instead our partners at Rockwell Collins are developing AADL specification and analysis tools to prove system-level properties at the architecture level.

[ Parent | on HN ]