Another Look at Provable Security

Post by nickpsecurity » Wed, Jul 22, 2015, 8:00 PM UTC

tptacek wrote: post #7

Some things that are important to remember: (a) "Proof of security" is a term of art that doesn't mean what it sounds like. In cryptography, you "prove" specific things about an algorithm, often in the context of a "game" with one or more adversaries. You need to know more than that an algorithm has a proof; you also need to know which proofs those are, and how they apply to your application. (b) Proofs generally app…

Good points. Far as code proofs, I think you should look at Microsoft's VerveOS (safety not security), seL4 (security), Astree, and the SPARK-based security projects. They all prove aspects of the code itself. The old A1 projects also typically mapped a low-level spec to code with many things at or near a 1-to-1 mapping. Very low risk of a misrepresentation or abstraction gap attack when done that way.

I still always encourage them to combine their efforts with thorough testing, code inspections, static analysis, and careful source-to-object code validation. Most of that is even required in the high assurance standards. Takes a lot more than proofs, code reviews, or tests in isolation to begin to make a strong security argument. As you know, it's so labor intensive and requires such specialist skills that almost all commercial and FOSS projects skip steps to get running code out the door. That's why penetrate and patch will always be the norm with highly secure systems always several versions worth of features behind mainstream. If they have them at all...

Post by nickpsecurity » Wed, Jul 22, 2015, 9:01 PM UTC

angry_octet wrote: post #20

nickpsecurity wrote: post #19

Earlier quoted context omitted.

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 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 VAX Security Kernel (A1 class). Pay special attention to the lay…

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_H... there is mention of an interesting tool/language called Spark Ada: http://www.spark-2014.org/ It makes me think that maybe my n…

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

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/

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

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/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. :)

Re: Another Look at Provable Security

Re: Another Look at Provable Security