It just says a method is 'proven'? How? Can someone please develop a piece of software, document/video themselves doing it and explain what/why they are doing parts of the project?
Basically walk a plebeian like me through making a program using formal methods.
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.
http://www.adacore.com/knowledge/technical-papers/safe-and-s...
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?
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:
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.
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
{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.
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.
(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.)
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:
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.
https://github.com/opencontrol/ https://github.com/opencontrol/compliance-masonry
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.
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)
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.
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.
http://cs.stackexchange.com/questions/13785/formal-program-v...
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;
}
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;
}
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.