3 ms·

Excellent idea in theory. Translating a formally verified system to actual application code is possibly the next frontier of system critical programming. A veri

by kartD 10y ago

Excellent idea in theory. Translating a formally verified system to actual application code is possibly the next frontier of system critical programming. A verified system along with a memory safe concurrent language should be able to avoid a significant set of common bugs. I hope to see some industry adoption.

nickpsecurity 10y ago
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.
- kartD 10y ago
  Sounds awesome! What kind of equipment is this done for (if you're comfortable answering) ?
  - nickpsecurity 10y ago
    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 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 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 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/SIGAda2003-Proceedings/Vendor-Esterel-SCADE-Suite-for-Ada.pdf 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.
    - kartD 10y ago
      Cool stuff, you're work sounds really cool.
      - nickpsecurity 10y ago
        That's others work. I dont do formal methods. Glad you enjoyed it though.
harveywi 10y ago
If you are interested in recent developments in verified programming, you might be interested in looking at Adam Chlipala's work (in particular, Bedrock [1]). His book "Certified Programming with Dependent Types" is a fantastic resource. Coq can be daunting to start with because it is three different programming languages in one: Gallina is the main pure functional programming language, Vernacular is a language of commands for controlling/guiding the proof assistant, and LTAC is the "type-level programming language on steroids" for writing type-level proofs. ("Type-level" is the important word here - the Curry-Howard correspondence allows us to encode propositions as types, and proofs are inhabitants of those types). When I was getting into certified programming, I found it helpful to try different proof systems until I could understand the common features. I found Microsoft's Lean Theorem Prover [2] to be quite user friendly and well documented, and I liked the syntax and feel. Also, trying out something bare-bones like Twelf [3] can help too, because there is not a lot of extra stuff tacked on and it is closer to an assembly language for machine-assisted proofs. For doing real-world things with Coq such as writing a simple web server, check out Guillaume Claret's blog [4]. Agda is comparable to Coq in terms of what they can do (I have heard). Idris is a "PacMan-complete" language that you might find useful for writing real-world programs, but I am not familiar with its suitability for programs relying on really complex proofs. Edwin Brady is writing a book on Idris [5], and you can get pre-release drafts through the Manning Early Access Program. [1] http://plv.csail.mit.edu/bedrock/ http://plv.csail.mit.edu/bedrock/ [2] https://leanprover.github.io/ https://leanprover.github.io/ [3] http://twelf.org/wiki/Main_Page http://twelf.org/wiki/Main_Page [4] http://coq-blog.clarus.me/ http://coq-blog.clarus.me/ [5] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...

by kartD 10y ago

nickpsecurity 10y ago

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.

kartD 10y ago
Sounds awesome! What kind of equipment is this done for (if you're comfortable answering) ?
- nickpsecurity 10y ago
  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 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 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 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/SIGAda2003-Proceedings/Vendor-Esterel-SCADE-Suite-for-Ada.pdf 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.
  - kartD 10y ago
    Cool stuff, you're work sounds really cool.
    - nickpsecurity 10y ago
      That's others work. I dont do formal methods. Glad you enjoyed it though.

harveywi 10y ago

If you are interested in recent developments in verified programming, you might be interested in looking at Adam Chlipala's work (in particular, Bedrock [1]). His book "Certified Programming with Dependent Types" is a fantastic resource. Coq can be daunting to start with because it is three different programming languages in one: Gallina is the main pure functional programming language, Vernacular is a language of commands for controlling/guiding the proof assistant, and LTAC is the "type-level programming language on steroids" for writing type-level proofs. ("Type-level" is the important word here - the Curry-Howard correspondence allows us to encode propositions as types, and proofs are inhabitants of those types). When I was getting into certified programming, I found it helpful to try different proof systems until I could understand the common features. I found Microsoft's Lean Theorem Prover [2] to be quite user friendly and well documented, and I liked the syntax and feel. Also, trying out something bare-bones like Twelf [3] can help too, because there is not a lot of extra stuff tacked on and it is closer to an assembly language for machine-assisted proofs. For doing real-world things with Coq such as writing a simple web server, check out Guillaume Claret's blog [4]. Agda is comparable to Coq in terms of what they can do (I have heard). Idris is a "PacMan-complete" language that you might find useful for writing real-world programs, but I am not familiar with its suitability for programs relying on really complex proofs. Edwin Brady is writing a book on Idris [5], and you can get pre-release drafts through the Manning Early Access Program. [1] http://plv.csail.mit.edu/bedrock/ http://plv.csail.mit.edu/bedrock/ [2] https://leanprover.github.io/ https://leanprover.github.io/ [3] http://twelf.org/wiki/Main_Page http://twelf.org/wiki/Main_Page [4] http://coq-blog.clarus.me/ http://coq-blog.clarus.me/ [5] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...