3 ms·

Do you have any links/references to the papers you mention?

nickpsecurity 11y ago
Most of the best papers are behind paywalls, unfortunately. I do have a small sampling on-hand from there and now that illustrate some of the high-assurance methods. http://www.iwia.org/2005/Schell2005.PDF http://www.iwia.org/2005/Schell2005.PDF Describes GEMSOS security kernel (A1 class) with nice graphics to illustrate the approach. http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf VAX Security Kernel (A1 class). Pay special attention to the layering of the kernel, coding strategy, and assurance section. http://cisr.nps.edu/downloads/sdm/SEKE08-Shaffer.pdf http://cisr.nps.edu/downloads/sdm/SEKE08-Shaffer.pdf Shaffer's Alloy technique elaborates a bit on how state machines are useful in security arguments, even without full formal. http://cryptosmith.org/docs/Lock-eff-acm.pdf http://cryptosmith.org/docs/Lock-eff-acm.pdf Costs and effectiveness of assurance activities for LOCK system (A1 class). http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf Modern effort (seL4) to exceed EAL7 by bringing verification to code itself. Note that some A1 projects had close to 1-to-1 spec to implementation mapping. So, full formal might be replaced by low-level, verified specs and matching code verified by inspection, etc. http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf Rockwell Collin's EAL7 framework for AAMP7G processor and CRYPTOL integration http://www.crash-safe.org/assets/verified-ifc-long-draft-2013-11-10.pdf http://www.crash-safe.org/assets/verified-ifc-long-draft-201... Previous work proved kernels supported MLS or MILS models. This is better given it's proving a hardware mechanism both enforces a security requirement and meets functional requirements. Significant given SAFE (see crash-safe.org) makes inherently secure apps easier to write. http://goto.ucsd.edu/quark/usenix12.pdf http://goto.ucsd.edu/quark/usenix12.pdf Proving security properties of a web browser. Typically, you know the work is legit if it spends time talking about the flaws formal verification caught. I don't see so much of that in this but they might have omitted that to publish what worked instead. http://www.cse.chalmers.se/~andrei/jsac.pdf http://www.cse.chalmers.se/~andrei/jsac.pdf A significant amount of recent work builds it in the language itself. http://web.archive.org/web/20130718103347/http://cygnacom.com/labs/cc_assurance_index/CCinHTML/PART3/PART36.HTM http://web.archive.org/web/20130718103347/http://cygnacom.co... Cygnacom's breakdown of Evaluation Assurance Level's is pretty nice. Shows the extra efforts put in and what you get. http://pastebin.com/y3PufJ0V http://pastebin.com/y3PufJ0V My framework compliments that and reminds that it must be applied to every layer down to the gates. So, although my sharing is limited by paywalls, I hope you find these interesting and can see the different perspectives of highly assured security. There have been numerous successes in independent testing, pen-testing, and field use. Also remember that this is only provable security rather than verification of properties in general. The field of verification and correctness assurance has progressed quite a bit (see CompCert, SPARK, Esterel, etc). Have fun.
- angry_octet 11y ago
  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. :)

Most of the best papers are behind paywalls, unfortunately. I do have a small sampling on-hand from there and now that illustrate some of the high-assurance methods. http://www.iwia.org/2005/Schell2005.PDF http://www.iwia.org/2005/Schell2005.PDF Describes GEMSOS security kernel (A1 class) with nice graphics to illustrate the approach. http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf VAX Security Kernel (A1 class). Pay special attention to the layering of the kernel, coding strategy, and assurance section. http://cisr.nps.edu/downloads/sdm/SEKE08-Shaffer.pdf http://cisr.nps.edu/downloads/sdm/SEKE08-Shaffer.pdf Shaffer's Alloy technique elaborates a bit on how state machines are useful in security arguments, even without full formal. http://cryptosmith.org/docs/Lock-eff-acm.pdf http://cryptosmith.org/docs/Lock-eff-acm.pdf Costs and effectiveness of assurance activities for LOCK system (A1 class). http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf Modern effort (seL4) to exceed EAL7 by bringing verification to code itself. Note that some A1 projects had close to 1-to-1 spec to implementation mapping. So, full formal might be replaced by low-level, verified specs and matching code verified by inspection, etc. http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf Rockwell Collin's EAL7 framework for AAMP7G processor and CRYPTOL integration http://www.crash-safe.org/assets/verified-ifc-long-draft-2013-11-10.pdf http://www.crash-safe.org/assets/verified-ifc-long-draft-201... Previous work proved kernels supported MLS or MILS models. This is better given it's proving a hardware mechanism both enforces a security requirement and meets functional requirements. Significant given SAFE (see crash-safe.org) makes inherently secure apps easier to write. http://goto.ucsd.edu/quark/usenix12.pdf http://goto.ucsd.edu/quark/usenix12.pdf Proving security properties of a web browser. Typically, you know the work is legit if it spends time talking about the flaws formal verification caught. I don't see so much of that in this but they might have omitted that to publish what worked instead. http://www.cse.chalmers.se/~andrei/jsac.pdf http://www.cse.chalmers.se/~andrei/jsac.pdf A significant amount of recent work builds it in the language itself. http://web.archive.org/web/20130718103347/http://cygnacom.com/labs/cc_assurance_index/CCinHTML/PART3/PART36.HTM http://web.archive.org/web/20130718103347/http://cygnacom.co... Cygnacom's breakdown of Evaluation Assurance Level's is pretty nice. Shows the extra efforts put in and what you get. http://pastebin.com/y3PufJ0V http://pastebin.com/y3PufJ0V My framework compliments that and reminds that it must be applied to every layer down to the gates. So, although my sharing is limited by paywalls, I hope you find these interesting and can see the different perspectives of highly assured security. There have been numerous successes in independent testing, pen-testing, and field use. Also remember that this is only provable security rather than verification of properties in general. The field of verification and correctness assurance has progressed quite a bit (see CompCert, SPARK, Esterel, etc). Have fun.

angry_octet 11y ago
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. :)