3 ms·

> Yet, you either don't or rarely need them in practice if goal is integrity or confidentiality rather than availability. My goal is correctness. A program tha

> Yet, you either don't or rarely need them in practice if goal is integrity or confidentiality rather than availability. My goal is correctness. A program that fails with a runtime exception is just as wrong as another that silently corrupts your data. Dijkstra put it very nicely: “We could, for instance, begin with cleaning up our language by no longer calling a bug a bug but by calling it an error. (...) The nice thing of this simple change of vocabulary is that it has such a profound effect: while, before, a program with only one bug used to be "almost correct", afterwards a program with an error is just "wrong" (because in error).” https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/E...

nickpsecurity 11y ago
Cute quote by Dijkstra that shows he hadn't quite figured out reality yet. So, correctness is your goal. That means you'll have to specify the behavior, safety/security policy, and prove the two equivalent. The implementation, both source and binary, will have to be shown equivalent along with proven free of language-level issues. Finally, you have to do that on triple, modular hardware [1] that's rad-hard w/ similar rigor in its lifecycle. Or use run-time checks [2] for each algorithm that can correct errors probably also on TMR or rad-hard board. Let's not forget the custom circuitry for RAM that works [3]. Darn, Dijkstra or not, you still need some kind of runtime checks and protection for correctness. :) [1] http://www.rockwellcollins.com/~/media/Files/Unsecure/Products/Product%20Brochures/Information%20Assurance/Crypto/AAMP7G%20data%20sheet.aspx http://www.rockwellcollins.com/~/media/Files/Unsecure/Produc... [2] https://galois.com/project/copilot/ https://galois.com/project/copilot/ [3] https://research.google.com/pubs/pub35162.html https://research.google.com/pubs/pub35162.html

nickpsecurity 11y ago

Cute quote by Dijkstra that shows he hadn't quite figured out reality yet. So, correctness is your goal. That means you'll have to specify the behavior, safety/security policy, and prove the two equivalent. The implementation, both source and binary, will have to be shown equivalent along with proven free of language-level issues. Finally, you have to do that on triple, modular hardware [1] that's rad-hard w/ similar rigor in its lifecycle. Or use run-time checks [2] for each algorithm that can correct errors probably also on TMR or rad-hard board. Let's not forget the custom circuitry for RAM that works [3]. Darn, Dijkstra or not, you still need some kind of runtime checks and protection for correctness. :) [1] http://www.rockwellcollins.com/~/media/Files/Unsecure/Products/Product%20Brochures/Information%20Assurance/Crypto/AAMP7G%20data%20sheet.aspx http://www.rockwellcollins.com/~/media/Files/Unsecure/Produc... [2] https://galois.com/project/copilot/ https://galois.com/project/copilot/ [3] https://research.google.com/pubs/pub35162.html https://research.google.com/pubs/pub35162.html