Hacker News Reader

Comment by nickpsecurity | Hacker News Reader

It's been going on in safety-critical field with groups like Rockwell-Collins and Eschersoft extracting to Ada/SPARK. Rockwell also compiles formally-verified CPU, the AAMP7G. My proposal was to extract to SPARK, Rust, C, and Java simultaneously since all the best static verifiers are for those. What one misses other will likely catch.

View on HN

Sounds awesome! What kind of equipment is this done for (if you're comfortable answering) ?

I work outside defense industry on purpose. No discomfort at all. ;) The remains of high-assurance safety and security fields are mostly used for defense (esp guards), aerospace, trains, private high-security, some industrial control (esp energy), some space, some medical, and plenty academics. Far as this conversation, here's an example of what I was talking about that mentions many others:

https://www.cl.cam.ac.uk/~mjcg/cambridge-wilding-sept08.pdf

Specifics on how they do EAL7 CPU and crypto here:

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

Eschersoft's tools below. They also have C analyzer.

http://www.eschertech.com/products/pd_and_spark.php

Specware from Kesterel Institute, like lots of their stuff, is pretty cool but I think efficiency dictates manual derivation of code. Gets you close to it, though.

ftp://ftp.kestrel.edu/pub/papers/specware/specware-jm.pdf

Esterel's SCADE w/ SPARK Ada below. Has huge list of application areas. I clearly forgot automotive in applicatino areas.

http://www.sigada.org/conf/sigada2003/SIGAda2003-CDROM/SIGAd...

Note: There's also been hardware synthesis from PVS and HOL specs. Most cool stuff like that is hard to get legally due to ACM/IEEE/Spring BS. I mention it so you know it's been done. I even saw one manual, formal verification of standard cells themselves. Getting close to the bottom. If my brain was whole, I'd be pulling out solid-state, physics books & doing HOL models of process nodes' molecules to get a jump on their asses lol.

Cool stuff, you're work sounds really cool.

That's others work. I dont do formal methods. Glad you enjoyed it though.

Reply on news.ycombinator.com