2 ms·

Very interesting reading. The whole notion of the AAMP7G processor is fascinating. Made solely for government in tiny quantities, in tightly controlled faciliti

Very interesting reading. The whole notion of the AAMP7G processor is fascinating. Made solely for government in tiny quantities, in tightly controlled facilities, probably rad hard, resistant to power analysis, etc. In this ppt http://usacac.army.mil/cac2/cew/repository/presentations/3_Hatcliff-SAnToS-Ft-Leavenworth-2008-07-09.pdf http://usacac.army.mil/cac2/cew/repository/presentations/3_H... there is mention of an interesting tool/language called Spark Ada: http://www.spark-2014.org/ http://www.spark-2014.org/ It makes me think that maybe my next study topic should be Spark or Esterel instead of Rust/Golang/some JS thing.

nickpsecurity 11y ago
Fine to learn for personal use but other stuff is better if you're job hunting. If you want to learn, then skip Esterel (big $$$) to learn Ada with AdaCore's free GNAT IDE. Helps to understand why it does certain things (eg foundations). Get that here: http://www.adacore.com/knowledge/technical-papers/safe-secure/ http://www.adacore.com/knowledge/technical-papers/safe-secur... AdaCore's "Gems" and other resources will help you plenty. SPARK is a variant of Ada designed to be easy to analyze with mathematical techniques with goal of automatically proving absence of certain bugs in over 95% of code. The article below has links to many resources and demonstrations. Tokeneer further demo's Praxis's Correct by Construction process, which is also cool. https://en.wikipedia.org/wiki/SPARK_%28programming_language%29 https://en.wikipedia.org/wiki/SPARK_%28programming_language%... Here's a nice example of applying it to a DNS server to prove absence of single-packet vulnerabilities leveraging common, coding issues: http://ironsides.martincarlisle.com/ http://ironsides.martincarlisle.com/ I'll end with a few other goodies. Adam Chlipala does great work in teaching and making formal methods lightweight. His book below describes such methods. More links in comments. https://news.ycombinator.com/item?id=9862127 https://news.ycombinator.com/item?id=9862127 Another high assurance processor below. Verified for correctness rather than security although one helps the other a bit. http://scidok.sulb.uni-saarland.de/volltexte/2006/633/pdf/Dissertation_9032_Dali_Iako_2006.pdf http://scidok.sulb.uni-saarland.de/volltexte/2006/633/pdf/Di... Sandia's Secure Processor (SSP), also called Score, utilizes a highly assured design and implementation that results in a Java processor immune to obvious code injection techniques or radiation-related issues. Their SEED architecture is really nice. Modern stuff is paywalled but this old paper tells plenty. Thing it leaves out, IIRC, is they use an ML-based hardware model to do equivalence checking between executable specification, hardware spec (in ML), and actual hardware HDL. Already in ASIC's on rad-hard processes. Availability of ASSET tools or SSP/Score unknown. ftp://ftp.cs.kent.ac.uk/people/staff/phw/.old-1999/tmp2/443-cpa2007-wickstrom.pdf Happy reading and bug hunting. :)

nickpsecurity 11y ago

Fine to learn for personal use but other stuff is better if you're job hunting. If you want to learn, then skip Esterel (big $$$) to learn Ada with AdaCore's free GNAT IDE. Helps to understand why it does certain things (eg foundations). Get that here: http://www.adacore.com/knowledge/technical-papers/safe-secure/ http://www.adacore.com/knowledge/technical-papers/safe-secur... AdaCore's "Gems" and other resources will help you plenty. SPARK is a variant of Ada designed to be easy to analyze with mathematical techniques with goal of automatically proving absence of certain bugs in over 95% of code. The article below has links to many resources and demonstrations. Tokeneer further demo's Praxis's Correct by Construction process, which is also cool. https://en.wikipedia.org/wiki/SPARK_%28programming_language%29 https://en.wikipedia.org/wiki/SPARK_%28programming_language%... Here's a nice example of applying it to a DNS server to prove absence of single-packet vulnerabilities leveraging common, coding issues: http://ironsides.martincarlisle.com/ http://ironsides.martincarlisle.com/ I'll end with a few other goodies. Adam Chlipala does great work in teaching and making formal methods lightweight. His book below describes such methods. More links in comments. https://news.ycombinator.com/item?id=9862127 https://news.ycombinator.com/item?id=9862127 Another high assurance processor below. Verified for correctness rather than security although one helps the other a bit. http://scidok.sulb.uni-saarland.de/volltexte/2006/633/pdf/Dissertation_9032_Dali_Iako_2006.pdf http://scidok.sulb.uni-saarland.de/volltexte/2006/633/pdf/Di... Sandia's Secure Processor (SSP), also called Score, utilizes a highly assured design and implementation that results in a Java processor immune to obvious code injection techniques or radiation-related issues. Their SEED architecture is really nice. Modern stuff is paywalled but this old paper tells plenty. Thing it leaves out, IIRC, is they use an ML-based hardware model to do equivalence checking between executable specification, hardware spec (in ML), and actual hardware HDL. Already in ASIC's on rad-hard processes. Availability of ASSET tools or SSP/Score unknown. ftp://ftp.cs.kent.ac.uk/people/staff/phw/.old-1999/tmp2/443-cpa2007-wickstrom.pdf Happy reading and bug hunting. :)