3 ms·

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

by kartD 10y ago

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.

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

by kartD 10y ago

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 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.