It's a slide deck, not a paper, but you might find this presentation from my class helpful: http://www.dwheeler.com/secure-class/presentations/Secure-So...

A specific example of software developed using formal methods is Tokeneer: http://www.adacore.com/sparkpro/tokeneer/

There's a severe lack of publicly-worked examples. Most formal methods applications are private, which inhibits improvement and use. I'm an advocate for the creation of more "open proofs" where the tools, software being proved, and the proofs are all available as open source software. If we had more open proofs then it'd be a lot easier to understand, apply, and improve them.

Ha! I just posted your FLOSS page in same thread. I appreciate work you did on high-assurance SCM and FLOSS summaries. I've been posting them for years in security forums to try to get some adoption. People still ignoring it with the reproducible builds fad being a recent example of people missing the bigger picture [that was already fleshed out in high-assurance field with methods that work, FOSS tools, and industrial examples].

Still an uphill battle but recent results are amazing. Do check out Myreen et al's work and COGENT's filesystem paper if you haven't seen them:

https://www.cl.cam.ac.uk/~mom22/

https://ts.data61.csiro.au/projects/TS/cogent.pml

I'll definitely give this a look.

I've been making posts every time this comes up and no one has been able to answer, or even quantify, what 'formal methods' where. The last time someone tried to sell me on them was accompanied by the pitch that "it means that your code proves itself that it's correct and that you will never have a bug ever"

Naturally I laughed at that as I can see someone peddling bullshit when I see it.

Do you mind if I email you about this powerpoint after giving it a look?

I believe the capability of ada to be formally proven was one of the reasons it has seen use in defence and real-time systems.

Well, there was the mandate plus the language itself was better than others at safety & programming in the large. The bigger reason, though, was that it was systematically designed to eliminate error from the syntax to memory handling to integrations. I mean, really thorough. Good description of all that in case anyone wants to cherry-pick safety features for use in a simpler language.

http://www.adacore.com/knowledge/technical-papers/safe-and-s...

Formal method means that the software can be formally proved to be correct (just like logic).

seL4 microkernel is formally verified, see: Comprehensive Formal Verification of an OS Microkernel, http://www.nicta.com.au/pub?doc=7371

It can be very costly to verify program after the fact, 250 lines of code per man-year is expensive. Program derivation is another way to do it, but it's also slow and significantly more complex process. Type systems, compilers and linters perform 'verification lite', they check statically for some easy to catch problems.

A Formal Method means to create a Formal System and construct a formal proof.

https://en.wikipedia.org/wiki/Formal_system

As a small example of using Hoare Logic, which takes every single command (aka line of code) in your program and turns it in to a Hoare Triple. A Hoare Triple looks like {precondition} command {postcondition}.

As an example let's prove the output is not 476.

    int numb;
    .....
    numb = numb * 2;  
    numb = numb + 1; 
    print numb

For print numb to print 476 we have the precondition that numb must be 476.

{numb = 476} print numb {We don't care what happens after you print}

If numb is 476 on the line above then the line before this one must have a post condition identical to this line's precondition.

{} numb = numb + 1; {numb = 476}

For this line to be true it must have a precondition that numb = 475

so {numb = 475} numb + 1; {numb = 476}

Again we chain this line's precondition to the previous line's post condition:

{} numb = numb * 2; {numb = 475}

Given that numb is defined as an integer there is no possible precondition capable of making this post condition true. We have formally proven this program is incapable of printing 476. Further since the stuff in the brackets can be as complex as we like we could have proven this program is incapable of printing even numbers.

https://en.wikipedia.org/wiki/Hoare_logic

Doesn't that rely on, often incorrect, assumptions of underlying hardware? Doesn't this change based on the environment that the system is going to be put in? There are things people are saying are "guaranteed" about formal systems that just aren't true.

To have a formal system actually be "correct" it needs to have never touched "incorrect" software or hardware. This contains, but is not limited to, a "correct" compiler and hardware implementation.

This is, I'd say, often not the case.

Right, whenever you try to use mathematics/logic to reason about the real world, you risk that some of your assumptions may be wrong. Every formally verified project will have some set of trusted assumptions. But hopefully this can still dramatically reduce software vulnerabilities---for example, systems more often fail because of bugs in the program logic than bugs in the x86 processor, so assuming a specification for the hardware and proving the program correct with respect to that should still be helpful.

(As an aside, hardware and compilers are actually comparatively tractable things to verify--the specifications are well-defined, and they are used by lots of clients so the effort to verify them pays off better. I think in the future, we are more likely to have unproven application programs running on top of proven compilers & hardware than the opposite.)

Here's the two, best books on it that I know of that are available for free:

http://adam.chlipala.net/cpdt/cpdt.pdf

https://www.cis.upenn.edu/~bcpierce/sf/current/index.html

Dependent-types are a more lightweight formal method. They're pretty useful as Chlipala et al showed in many developments. IDRIS and ATS languages use them for systems. Software Foundations is about the full thing.

Tried to find you an easy intro. Harder than I thought. However, this PowerPoint is an excellent intro to formal specifications in terms of what they are, why you want them, and many examples.

http://www.cs.nott.ac.uk/~pszrq/files/1FSPintroduction.ppt

Once you see that, it becomes obvious that proving implementation matches such specs is beneficial. Took an hour to find an intro to that which was worthwhile and easy to digest. Here's one:

http://www2.imm.dtu.dk/~aeha/Railway/index/TSnotat.pdf

Anyone following along that wants a list of tools, esp open-source, should check out Wheeler's reference on high-assurance FLOSS:

http://www.dwheeler.com/essays/high-assurance-floss.html

I'm about to start reading "The Little Prover" (https://mitpress.mit.edu/books/little-prover) which sounds like a good intro.

The Amazon reviews on it look good. I like how it's very incremental and more manual than modern provers. The latter being advantages as the beginner will have a glimpse of what they're doing or why. I might order a copy.

Take your software.

Rigorously define security goals ("no user can see another user's file; no input can cause this handler to access variables other than this specific list").

Convert all or, more likely, part of your program into a model; for instance, predicate logic.

Run analysis tools to verify that the model achieves the security goals. Once expressed in a mathematical model, "proving" it becomes a search problem, achievable with code. Intuition and cleverness can, if your model is accurate and complete, be eliminated.

It's sort of the software security equivalent of teaching a computer to play chess.

This was already started by 18F. If you haven't heard of them, they are the first U.S. federal gov digital consultancy, and the primary force behind a lot of security/certification improvements already.

https://github.com/opencontrol/ https://github.com/opencontrol/compliance-masonry

This stuff is neat, but it's more of a formal methods approach to security management than it is to reducing software vulnerabilities.

To apply formal methods to software development, you do one of two things:

* You transform code in conventional programming languages into machine-readable formats understood by model checkers

* You write your code in a language that itself admits to being model checked.

I appreciate this link, though; I was unaware of what 18F was doing here.

I'm pretty sure what you're talking about exists in the OpenControl repos somewhere-- I'm just not sure which one (sorry). My former 18F colleague was recently talking about translating controls about password specifications into actual automated tests on the codebase and/or app.

The reason all that "formal methods" stuff is in there as well (and indeed it's what the more prominent repos in there are about) is so that we can eventually connect the dots between effective security practices in code and the management of the security controls on the administrative side, and at least until the former catches up to the software methods, take the manual work of generating the copious documentation regarding all of this out of the developers' hands. Case in point: https://compliance.cloud.gov/ (<- all auto-gen, AFAIK)

> Can someone please develop a piece of software, document/video themselves doing it and explain what/why they are doing parts of the project?

iirc I think Leslie Lamport might've been thinking about making just such a series on TLA+ on the ML... TLA+ is a software specification system he wrote that was popularized by Amazon and Microsoft. It's open and the tools, while rough, are free to use.

If he doesn't go through with it I've been looking for something to teach and I'd like almost nothing more than to teach TLA+ to more people.

I'm no expert but the way I understand it is you are mathematically proving certain things about the software. Basically you prove that there won't be a division by zero or buffer overflow or whatever in a certain function.

Usually there are extensions to programming languages that let you annotate these proofs and software can check it for you.

Like with unit tests you only get these assurances if you write out the proofs. Historically writing them has been really time consuming, but the paper claims it is getting much more convenient.

Some of the methods they list (like SAT solvers and model checkers) mostly obviate the actual proving part for simple statements. Instead you only need to input what you want to prove, and the computer attempts to find a proof or disproof. For many of the things you would want to prove in software, this is sufficient.

Here is a paper by the AWS team that describes their approach to formal methods and which you could find 'tangible' : http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

Not exactly what you're looking for, but maybe a good starting point

http://cs.stackexchange.com/questions/13785/formal-program-v...

Recent article and discussion: https://news.ycombinator.com/item?id=12612856 (A Hoare Logic for Rust)

Program proofs can get arbitrarily clever/complicated.

But one of the fundamental maneuvers is to examine the full input space of a given function, and assert that the fully output space of a function has certain properties, which then may get fed in to later uses of the results of that function to further assert things.

The "full input space" of a function is generally what you'd expect it to be, but the "full output space" of a function is worth discussing. It is not just the return values of the function in the sense the local language means, it is also the full state of visible changes to the environment, any exceptions, etc. So, for instance, in the psuedocode function

     // "int" is the conventional wrapping machine int here
     function sample (int x, int y) int {
         if (x == 25) {
             throw DontLike25Error("I can't stand the number 25")
         }
         if (y == 0) {
             external yZeros; // imagine I'm importing a global variable
             yZeros++;
         }
         return x + y;
     }

A human programmer will conceptualize this as "a function that sums two numbers with a weird bug", and probably ignore the yZeros entirely. A prover sees this as a function that "returns the exception DontLike25Error OR returns a new yZeros and the wrapped sum of the two input values". You generally conceive of exceptions as a return value, and global variable updates as a new value, etc.

So, if you want to prove a function will never divide by zero, it is at least conceptually a case of iterating over all possible inputs and verifying that the property holds that a DivideByZero exception is never returned:

     function divide (num float, denom float) float {
         if (denom == 0) {
             return 0; // actually a bad idea, but bear with me
         }
         return num / denom;
     }

We can now easily prove this never divides by zero, because we can examine all the possible nums and denoms and verify we always get a "float".

At least... if == 0 correctly detects all possible zeros, including the local negative zero if applicable, and doesn't return true for any other possible float value, and if the division operator doesn't yield a DivisionByZero for any other value accidentally or deliberately. And our proof system would still have to bear in mind the possibility of underflow (a non-zero numerator may still yield a 0 if the denominator is sufficiently large) or possibly an Inf overflow if the denominator is sufficiently small.

And with that paragraph, you begin to see both the problems with creating proof systems, and using them. We programmers want to slop down a division operator and assume that it's going to divide two numbers and yield a third number and we don't want to care about the exceptions. A proof system makes you care. As the program scales up, this only gets more interesting; the previous paragraph was just about one usage of the division operator. Pretty much every operator and function you've ever used comes with a similarly intense list of caveats, exceptions, and weirdnesses if you want to be really rigorous about what happens in your code. Especially including things like "allocating memory" or "allocating disk" as functions, which even before we're trying to prove things are often so difficult to deal with we programmers just punt entirely.

From these simple building blocks, you can start building you way up to more interesting assertions. But this is the foundation that the whole system is built on.

It's also worth pointing out that from this point of view, a prover is doing what even the sloppiest programmer is doing in their head anyhow. You have to at least to some extent be thinking about what goes into a function and exactly what comes out. You just probably aren't considering anywhere near all the options. But you must be thinking like this in some manner, no matter how incompletely and sloppily, to be a programmer at all. Proving things about code is less foreign than it should seem at first.

You can also even see how dynamic languages can start being difficult to deal with at scale if you don't apply a lot of discipline external to the dynamic language itself, because dynamically-typed languages have very "large" functions when you view them this way; with no way to constrain the inputs, it can be difficult to "range across all possible inputs" conceptually. This has perfectly practical real effects for things like tracing optimizing interpreters, which must in principle always be verifying incoming types to functions in a way a static language doesn't need to, no matter how optimized that check may be in practice.

You can put your toe into this world simply by learning how to use your type system to its maximum power. Type systems are in general not all that powerful compared to what a full prover can prove. (Not even Haskell's.) But it's a start, and it's relatively easy, and has good bang for the buck.

Incidentally, once you start looking at your code this way, it becomes obvious why functional programming is much easier to prove things about; in the purest case, you can't get surprise global variable updates and you don't get random unions of what can be returned by a function with things like "exceptions". You've got many fewer cases to worry about because the functions are what their type signature says they are, instead of their type signature unioned with a large set of exceptions unioned with arbitrary IO unioned with arbitrary global variable updates unioned with arbitrary code updates (in dynamic languages). However, this pretty image is often not fully realized; even Haskell can throw exceptions anywhere, even if it is discouraged. For math reasons, Haskell programmers say anything can be "bottom", which is this additional "crash" value that Haskell doesn't eliminate.