Building High Integrity Applications with SPARK

Category: Hardware & DIY
Author: John W. McCormick, Peter C. Chapin
5.0
This Year Hacker News 4
This Month Hacker News 1

Comments

by nickpsecurity   2018-11-20
If you want to learn it, here's the main book people are using:

https://www.amazon.com/Building-High-Integrity-Applications-...

by nickpsecurity   2018-03-27
They probably should've started with a Wirth-style language plus Design-by-Contract and static analysis. That would knock out tons of stuff at compile and runtime. If looking for mature language, the best one for predictability is SPARK Ada hands down. It was designed for easy analysis in automated provers. It's automation level is a lot higher than it used to be. Folks wanting provable programs should either be considering using it or prototyping their programs in it with semantics-preserving translation to the blockchain language/VM.

https://www.amazon.com/Building-High-Integrity-Applications-...

Note: The book is designed for people without formal methods background. I can't say how easy or not it will be since I just got it. :)

Are we there yet? 20 Years of Industrial Theorem Proving with SPARK

https://proteancode.com/keynote.pdf

IRONSIDES DNS illustrates it can handle bigger problems

http://ironsides.martincarlisle.com

Frama-C and SPARK both build on Why3 platform with its intermediate language WhyML. Work built on any of these three can usually be ported to the others. So, I'll drop a recent example in Frama-C that's really math heavy with a style amenable to high automation.

https://hal.archives-ouvertes.fr/hal-01681134/document

by nickpsecurity   2018-01-07
[Copying/pasting my reply to author in Disqus since at work. ]

Good write-up on the difficulties. The first I saw was Guttman’s paper that set back the hype quite a bit:

https://www.amazon.com/Building-High-Integrity-Applications-...

Here’s my recommendation in general. Learn lightweight methods such as Meyer’s Design-by-Contract for most stuff, TLA+ for concurrency/order, Alloy for structure, SPARK for low-level code, and so on. TLA+ on distributed stuff seems to sell people the most. With a formal method in hand, then apply this methodology: memory-safe language + lightweight method to model-check important stuff + Design-by-Contract + tooling to generate tests from specs/contracts + fuzzer running with runtime checks enabled. This combination will bring the most quality improvement for least effort. In parallel, we have the experts formally verifying key components such as kernels, filesystems, network stacks, type systems, compilers, security protocols, and so on. They do so modelling real-world usage with each one coming with contracts and guidance on exactly how they should be used. The baseline goes up dramatically with specific components getting nearly bullet-proof.

Also, you said you wanted entire system to be reliable. There was one that set the gold standard on that by noting how everything failed with systematic mitigations for it in prevention and/or recovery:

http://www.hpl.hp.com/techreports/tandem/TR-85.7.pdf

https://en.wikipedia.org/wiki/NonStop_(server_computers)

The OpenVMS clustering software alone let their systems run for years at a time. One ran 17 years at a rail yard or something supposedly. The NonStop systems took that to hardware itself with them just running and running and running. Applying a combination of balanced assurance like I describe, NonStop techniques for reliability, and Cambridge’s CHERI for security should make one hell of a system. You can baseline it all with medium-assurance using tools that already exist with formal verification applied to a piece of the design at a time. The work by Rockwell-Collins on their commercially-deployed AAMP7G’s shows that’s already reachable.

http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf

So, there’s you some weekend reading. Merry Christmas! :)

by nickpsecurity   2018-01-07
“but after studying many other ICO, I am convinced now that this is not just a short-lived fad, but a real new model to fund projects, and especially open-source projects related to blockchains.”

There’s been quite a few of us suggesting people jump into blockchain just to get funding for more important stuff (e.g. language-level tooling or libraries) they’ll produce as part of the coin offering they sell to investors. Plus, with the focus on correctness, it’s easier than ever to get the private sector to invest in high-assurance tooling. Problem is they keep trying to clean-slate everything when there's piles of work to build on with better benefits in the long term. And this work is hard even when doing simple things if you want end result to be widely usable. So, you better have a good justification for trying to redo decades worth of hard work on your own with some VC funding.

Anyone wanting a shortcut should build your language on top of capabilities of the SPARK Ada language [1] with this book [2]. Your smart contracts get all the benefits it currently offers plus whatever extra you build plus whatever they build with the influx of money for Pro edition. Recent projects already add some pointer [3] and floating-point [4] safety to what they already mostly automate with that tooling. This is also a mature tool whose development and commercial use goes back decades [5].

[1] https://www.amazon.com/Building-High-Integrity-Applications-...

[3] https://arxiv.org/abs/1710.07047

[4] http://lists.forge.open-do.org/pipermail/spark2014-discuss/2...

[5] http://www.spark-2014.org/uploads/itp_2014_r610.pdf