Dramatically Reducing Software Vulnerabilities [pdf]

This is prevalent in the embedded OS market with vendors that sell commercial Linux licenses. Many will take a stable Yocto distribution and strip out unnecessary pieces to reduce its weight to suit customer specifications.

Often times the OS vendor will then have to go in and add code to meet standard/certification requirements set by the customer. They'll also generally have to add certain libraries and snippets of code for hardware/middleware-specific integration.

I'm not an embedded engineer, but from my convos with engineers/execs I have to believe its exceedingly rare that a company could simply strip out pieces from an open source distribution, not add anything proprietary, and sell the resulting code to a customer.

http://projects.cerias.purdue.edu/poly2/

Especially see Section 3.6 of the main paper:

https://www.acsa-admin.org/2003/papers/72.pdf

It's an old technique of mine, too. Just edit out all that shit so it returns with an error message telling me what the hackers were trying to use with whatever access they got and from where. :)

https://www.imperialviolet.org/2015/10/17/boringssl.html

Seems like it's been a useful concept.

Which is fine for you to do of course but it is probably inaccurate to assign no value to the code you are removing. Someone took the time to write it. People don't spend their time writing code for no reason. That code may have no value to you personally but it has value to someone.

OpenBSD project seem to be doing the right thing (as they always did, imho) by deleting a lot of code from the base and not letting it to rot.

Less code = less complexity, less side effects, less maintenance, and less bugs.

Sure, you have to do it without loosing any useful functionality. As a software ages, it becomes bloated, there is a lot of copy'n paste, features aren't useful anymore because the business changed.

On page 15, you can see Rockwell-Collins combining model-driven development with Z, SPARK, and state-machines. It's a nice example of power of interacting, state machine approach combined with some other elements.

https://www.nsa.gov/resources/everyone/digital-media-center/...

http://langsec.org/

There are lots of compelling ideas there (and LANGSEC researchers would tend to agree that if a functionality can be implemented correctly as an FSM, that would be a safer option).

A related phenomenon that people talk about is the unexpected Turing-completeness (where people have been able to prove that so many different parts of computing are Turing-complete -- things that were never intended to be programming languages). LANGSEC people and others refer to the negative security implications of some of this as "weird machines", where you really didn't want Turing-completeness but you got it by accident or by default anyway, and it might be possible for an attacker who can corrupt control flow or other kinds of state to then perform arbitrary operations. For security people an example may be return-oriented programming, but there are evidently others that can be thought of in the same way.

Debugging is particularly straightforward - events cross states, yo. :) All you need is logging. Event detection code is particularly amenable to rigorous verification.

Toolchains like ObjecTime and Rational Rose had direct support for "coding using graphic representations of FSM" but the tools themselves were somewhat unwieldy and expensive and they sort of dinosaured.

But how would we incentivize businesses properly to be [WHATEVER] compliant, and pay for the regular security scans? Social proof / public shame hasn't worked yet, despite MANY high profile examples. We may have to impose some sort of carrot/stick combo that says: "If your infrastructure consists of N# of networked devices, you must meet these standards. If you fail to, and get caught in a data breach (like what happens with PCI), fines that could put you out of business get levied. Additionally, if you show proof of your security certification every year, you get a tax break."

Best practices also drift over time and vary with context. A challenge is that there are very old, very large code bases where as a practical matter will never be modernized because it is tantamount to a rewrite, with all of the bug creation and cost implied.

Robust software is definitely possible today even in languages like C++, but the development process for software that rarely fails isn't that compatible with the popular "fast iteration" development model nor the current computer science skills of most software engineers.

But this is what OpenControl is meant to solve. https://github.com/opencontrol/

http://lukemuehlhauser.com/wp-content/uploads/Bell-Looking-B...

I wrote a post on Schneier's blog describing a few ways security evaluation has been done plus how I would do it:

https://www.schneier.com/blog/archives/2014/04/friday_squid_...

My model can be used for regulations or liability. Another proposal I had was enforcing a minimum amount of assurance activities proven to knock out defects. Likely a subset of techniques in this post:

https://news.ycombinator.com/item?id=10734477

Note that U.S. government has already given prior guidance on robust software that mentioned some of those with specific tools. A number of companies in safety-critical are doing things like formal specifications for precise requirements, review of various items in lifecycle, automated generation of tests covering every path, and implementation in Ada/SPARK to knock out classes of errors there. There's also tools like Softbound+CETS plus minor modifications to processors that make most classes of errors or attack impossible. So, it's not theoretical so much as something practical that many avoid for convenience or extra profit. ;)

I'd rather a professional guild makes the call on what other capital-E Engineering disciplines call, the state of the art, is. We do have something like that, a document published under the IEEE called SWEBOK [0]... but it needs greater industry adoption and a the establishment of a profession that governs our ethics, IMHO. Presently it's nice to know but my employer pretty much dictates what corners I will cut and what mistakes are acceptable, etc. Since there's no liability involved and no actuaries adjusting the insurance rates based on our technology and process choices my employer doesn't have an immediate dollar-figure that gives consequence to those risky decisions.

[0] https://en.wikipedia.org/wiki/Software_Engineering_Body_of_K...

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

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.

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.

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.

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.

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.

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

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.

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

So it's not unreasonable for NIST (which actually wants people to enjoy computer security) to investigate what could be done in this area!

Edit: but it's true that it would be awesome to see government do something to make these improvements actually happen -- and a research report probably isn't that.

After reading one may think: Why the fuck is there any dynamic memory allocation (stack) going on there? Why isn't the car software implemented as one big pre-allocated hierarchical state machine? You wouldn't expect such execution dynamism in hard circuits or even FPGAs. But in any case I think non-deterministic systems (especially complex CPUs+programs) should be outlawed for such mission critical signal paths.