3 ms·
...and just to provide an example of how one does verification with for C: https://galois.com/blog/2013/09/high-assurance-base64/ https://galois.com/blog/2013/0
by cbsmith 11y ago
...and just to provide an example of how one does verification with for C: https://galois.com/blog/2013/09/high-assurance-base64/ https://galois.com/blog/2013/09/high-assurance-base64/
- nickpsecurity 11y agoI just did it Orange Book B3/A1 style by visual, result, and trace-based correspondence between code and executable specifications. Plus lots of FSM's. Next project I'd add Frama-C and Astree for code-level verification. Plus, CompCert for compilation with more result & trace-based simulation for correspondence. Good to see new work, though. I follow Galois' stuff a lot because they're very innovative and practical. Harden et al are also using LLVM simulations for correctness but with ACL2.