Hacker News Comments on
Building High Integrity Applications with SPARK
·
4
HN comments
- This course is unranked · view top recommended courses
Hacker News Stories and Comments
All the comments and stories posted to Hacker News that reference this book.Yep, here some very good books about it, specially relevant given the main subject."Building High Integrity Applications with SPARK"
https://www.amazon.com/Building-High-Integrity-Applications-...
"Building Parallel, Embedded, and Real-Time Applications with Ada"
https://www.amazon.com/Building-Parallel-Embedded-Real-Time-...
"Embedded Software Development for Safety-Critical Systems"
https://www.amazon.com/Embedded-Software-Development-Safety-...
There's tooling like Cryptol and SPARK to make this a lot easier than it was in the past. Cryptol can generate software or hardware that implements the high-level spec of the algorithm. Far as practical use, certainly not just one even though still extremely rare. Here's some more:Altran/Praxis Correct-by-Construction for a cert authority
http://www.sis.pitt.edu/jjoshi/Devsec/CorrectnessByConstruct...
Same company ports Skein from C to SPARK, finds trouble
http://www.skein-hash.info/sites/default/files/SPARKSkein.pd...
SPARK Ada is available under GPL and commercial licenses. The book below is quite easy to read compared to most stuff with formal methods. The companies building stuff like this usually also have tools to generate tests (property-based testing) from contracts/specs and can automatically turn anything you can't prove into runtime checks. Shocked it's not used more often in areas like smart contracts or cryptocurrency protocols.
https://www.amazon.com/Building-High-Integrity-Applications-...
Galois built Cryptol for NSA but open sourced it.
Rockwell Collins built SHADE and some other tools for high-assurance crypto. They build stuff for the defense sector mainly funded by NSA. They even have a separation-preserving, verified CPU.
If you're learn Ada, be sure to check out Building High Integrity Applications in SPARK to get the most benefit from it. I also find Barnes book does a good job chapter by chapter showing how it's systematically designed for safety. Finally, if anyone doubts improvements that can happen, I have the most apples to apples study you'll see comparing Ada and C.https://www.amazon.com/Building-High-Integrity-Applications-...
What makes this a good write-up is you could give it to a project manager as quickly as an engineer. An updated version of this with links to current tech, esp low cost or easy to integrate, might be worthwhile. Other improvements since then include generating tests directly from the contracts, using contracts with automated provers, leaving contracts in as runtime checks while throwing fuzzers at that code, and using contracts for bug repair. They can't do everything but they're a very high-ROI technique with some immediate benefits plus maybe some down the road if your software/company gets bigger.Write-ups or examples of some of the above:
https://hillelwayne.com/post/pbt-contracts/
http://www.skein-hash.info/sites/default/files/SPARKSkein.pd...
https://www.amazon.com/Building-High-Integrity-Applications-...
https://blog.adacore.com/running-american-fuzzy-lop-on-your-...
https://www.microsoft.com/en-us/research/wp-content/uploads/...