| Hansen et al were first I think
http://brinch-hansen.net/papers/ Notes: He sprinkles references to method in various papers. Design Principles is one I think. He says the work like COBOL compiler and RC 4000 was coded in assembler. Yet, he and compiler group wrote it by hand in ALGOL to better analyze, structure, and extend these systems. So, an ALGOL form for understanding and hand-written assembler for optimal execution. Gypsy Verification Environment for high-assurance security - Overview and Example
https://www.cs.rice.edu/~dwallach/courses/comp527_s99/gypsy-...
ftp://ftp.cs.utexas.edu/pub/AI-Lab/tech-reports/UT-AI-TR-78-11.pdf Notes: Gypsy was one of more developed methods for high-assurance security back in the day. Used in A1-class SCOMP system and more. The usage in A1 was to do two versions of system in parallel: one in Gypsy for use with provers, info flow analysis, and so on; one in actual code that would run on system. Problems in one could often tell you something about the other. 4GL combining BASIC, LISP, and C
http://lost-in-triple-HD-failure :( Notes: This was mine cuz I hated C and C++ but liked industrial BASIC's I started with. Made a dumb, but effective, translator from one BASIC to C and/or C++ (memory fuzzy there). Let me iterate rapidly & safely then have portable C + safety checks automatically in when done. Started adding custom commands 4GL-style to eliminate boilerplate. Upon finding LISP, but not really learning it, I ported tools so I basically coded a 4GL BASIC in LISP w/ per-function compilation, easier parsing, macros for easy 4GL stuff, and extraction to C or C++. Always two forms of the code in place: one for development/analysis; one for production. Crazy RAD pace w/ usually safe, efficient results. I really miss my tool as I'm too brain-damaged to recreate it now. Nim has many of its attributes, though, so there's hope. :) Adam Chlipala's Certified Programming book/work and Bedrock
http://adam.chlipala.net/ Notes: This method is quite loaded. You can use a theorem prover and dependently-typed language to express your program in a way that catches all types of problems. Usually extracts to ML that you might hand-optimize. Alternatively, reminiscient of Hansen, you can do low-level coding in Coq via Bedrock that's basically a safer, assembly language. Microsoft's Coq ASM and another's TALC typed ASM do similar stuff. seL4 verification method
http://concrete-semantics.org/ Notes: Someone told me above book teaches you what skills they used. Google AutoCorres for C-to-HOL extraction part. Anyway, their method is to develop in Haskell and C simultaneously for separation kernel. The Haskell forms the abstract specification that easily feeds into HOL for analysis of basic function and security. The C obviously is the running code. They go further than Gypsy by using AutoCorres to extract HOL from C then proving Haskell and C HOL specs are equivalent. Might look for C-level problems, too, but don't recall. Bootsafe - Develop Forth firmware in Java for safety
http://slideshowes.com/doc/437272/efficient-code-certificati... Notes: One of military's funded projects to improve security. Open Firmware specifically. Many firmware, including OF, is in the flexible and fast but unsafe language Forth. The Java language is safer, easy to analyze, easy for experienced to compile, and has no business in firmware w/ its big-ass runtime. :) BootSafe lets security engineers code and analyze firmware in Java then extract that in a verified way to executable Forth. Online presentations are all partial and crappy w/ this most detailed I found. It's a finished product from atcorp.com, though. Notice one could manually do this, too, w/ side-by-side developments with C, C++, Java, or SPARK. Further evidence is that many embedded MCU developers code in C or C++ with mockups of MCU assembler or interfaces. Claim much better results in maintenance & defect reduction. Another old one of mine - safe or fast? choose two
(no website link) Notes: The idea was that many development or analysis tools should be implemented in as safe and sound a fashion as possible. However, that usually meant sloooow. Development, to maximize flow, needs to give immediate results to programmer if possible. So, for each tool or app, build two versions of it with logical equivalence: safe and fast. The fast is used for day-to-day development. The safe one is used overnight or if problems show up in fast that are resisting debugging (eg might be in compiler/lib). Example combos included MLton with FLINT or CakeML compilers, Racket dialect with PreScheme/VLISP, and CompCert C and/or Softbound+CETS with GCC/LLVM. Batches run overnight to create safe versions of any changes or commits. Batches also re-run tests from fast versions to ensure they match safe versions. Another of my proposals - C, Java, Ada/SPARK, and ML/Haskell
(no website link) Notes: There's many static, dynamic, and formal analysis tools for C that catch specific types of stuff. Same for Java including basically all the great analyzers for concurrency errors. The best pushbutton analysis is in SPARK for Ada which also has design-by-contract for interface checks. There are ML's with dependent types, easy covert channel analysis, easier formal verification, and so on with Haskell having similar tools. One of my concepts... for where it matters most... was implementing algorithm or system in at least two of these simultaneously with a max of four. In lowest common denominator and consistent way of course. Then, apply at least two of best tools for each language to system. Any flaws found in one are checked in others. Result, from eyeballing to static analysis to auto-testing, will probably be the most thorough assurance you can get without being a formal verification expert. You can do that too, though. Not sure how practical it is. I think it would be easy with 4-5 person team of specialists w/ good communication with probably interesting results. |