10 ms·

Dramatically Reducing Software Vulnerabilities [pdf]

132 points by Dowwie 10y ago

gravypod 10y ago
This is an interesting read. Despite this, I still cannot understand what a Formal Method is. 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.
- adrianN 10y ago
  Not exactly what you're looking for, but maybe a good starting point http://cs.stackexchange.com/questions/13785/formal-program-verification-in-practice http://cs.stackexchange.com/questions/13785/formal-program-v...
- quantumhobbit 10y ago
  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.
  - johncolanduoni 10y ago
    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.
- dwheeler 10y ago
  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-Software-10-Formal-Methods.ppt 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/ 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.
  - retox 10y ago
    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.
    - nickpsecurity 10y ago
      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-secure-software-an-invitation-to-ada-2012/ http://www.adacore.com/knowledge/technical-papers/safe-and-s...
  - gravypod 10y ago
    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?
- joshmarlow 10y ago
  I'm about to start reading "The Little Prover" (https://mitpress.mit.edu/books/little-prover https://mitpress.mit.edu/books/little-prover) which sounds like a good intro.
  - nickpsecurity 10y ago
    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.
- tptacek 10y ago
  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.
  - alaithea 10y ago
    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/ https://github.com/opencontrol/compliance-masonry https://github.com/opencontrol/compliance-masonry
    - tptacek 10y ago
      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.
      - alaithea 10y ago
        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/ https://compliance.cloud.gov/ (<- all auto-gen, AFAIK)
- jerf 10y ago
  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.
- nabla9 10y ago
  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 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.
- stonemetal 10y ago
  A Formal Method means to create a Formal System and construct a formal proof. https://en.wikipedia.org/wiki/Formal_system 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 https://en.wikipedia.org/wiki/Hoare_logic
  - gravypod 10y ago
    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.
    - vilhelm_s 10y ago
      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.)
- agentultra 10y ago
  > 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.
- nickpsecurity 10y ago
  Here's the two, best books on it that I know of that are available for free: http://adam.chlipala.net/cpdt/cpdt.pdf http://adam.chlipala.net/cpdt/cpdt.pdf https://www.cis.upenn.edu/~bcpierce/sf/current/index.html 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 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 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 http://www.dwheeler.com/essays/high-assurance-floss.html
- udkl 10y ago
  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/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/fo...
- jk4930 10y ago
  Recent article and discussion: https://news.ycombinator.com/item?id=12612856 https://news.ycombinator.com/item?id=12612856 (A Hoare Logic for Rust)
jefffoster 10y ago
I wonder if this'll (or something like it) be the tipping point for governments to introduce more regulations for software? We already have regulations like PCI-DSS for dealing with payment card, maybe this'll end up with regulations for dealing with security? The conclusion suggests better specification, better testing and more resilient architectures are the strategies that could make a difference. Perhaps software engineering will have to agree on a set of "best" practices that make security problems less likely to occur? (typos)
- mildweed 10y ago
  I can definitely see more standards and certifications coming to pass, which then later distill down to one or two primary certifications that everybody aspires to get. Currently there are multiple privacy/security standards (PCI, HIPPA, FERPA, etc). We'll probably have to get more opinions from more sensitive-data industries, and then for them all to find the common ground. 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."
  - ryanmarsh 10y ago
    Regulatory enforcement. Even though PCI DSS is enforced by a private regulatory body, it still carries weight. HIPAA has HHS which does investigate and lead to corrective action. Both of these bodies scare the crap out of a lot of companies. I've worked in both sectors (banking/credit, healthcare) and the fear is palpable. If the CFPB had the ability to enforce regulatory requirements for handling of PII you bet your ass companies would fall in line. Nobody wants trouble with the feds.
    - schoen 10y ago
realkitkat 10y ago
Although it does mention some risks of using 3rd party code/components in passing under 'Understanding and Controlling Dependencies' (835-), I would have expected them to make a stronger case for OWASP 2013-TOP10-A09: 'using components with known vulnerabilities'[1] type of analysis. This applies to almost any kind of modern application, not just web apps, but especially to those written in native languages (C/C++/...) as we increasingly build our applications by bringing in varying amounts of 3rd party code; open source or commercial. Like traditional static code analysis, more or less mature tooling exists in open source[2][3][4] and commercial capacity to perform static binary and source code analysis to discover and track 'offending' 3rd party code, which does make it practical to include this kind of analysis to sdl/sdlc/devops workflows. [1] https://www.owasp.org/index.php/Top_10_2013-A9-Using_Components_with_Known_Vulnerabilities https://www.owasp.org/index.php/Top_10_2013-A9-Using_Compone... [2] http://www.binaryanalysis.org/en/home http://www.binaryanalysis.org/en/home [3] https://www.owasp.org/index.php/OWASP_Dependency_Check https://www.owasp.org/index.php/OWASP_Dependency_Check [4] https://github.com/OWASP/SafeNuGet https://github.com/OWASP/SafeNuGet
roymurdock 10y ago
Goal: The goal of this report is to present a list of specific approaches that have the potential to make a dramatic difference reducing vulnerabilities – by stopping them before they occur, by finding them before they are exploited or by reducing their impact. Impetus: In response to the February 2016 Federal Cybersecurity Research and Development Strategic Plan, NIST was asked to identify ways to dramatically reduce software vulnerabilities. NIST worked with the software assurance community to identify five promising approaches. This report presents some background for each of the approaches along a summary statement of the maturity of the approach and the rationale for why it might make a dramatic difference. Further reading was provided for each approach. Hopefully other approaches will be identified in the future. Current Cybersecurity Approaches: 1. Formal Methods - how do you check your program while writing code? (static analysis, model checkers, pragmas, model-based programming, and more recently contracts) 2. System Level Security - how do you partition components in a system? (containers/hypervisors/virtualization with smart API calls) 3. Additive Software Analysis - how do you analyze completed software to check for problems? (expression and exchange standards, better IDE plugins, advanced static analysis tools) 4. Mature Development Standards - how can you modify and reuse tried and tested code? (find, understand, learn, and combine the most relevant frameworks) 5. Moving Target Defense & Artificial Diversity - how can you minimize your program's attack surface? (compile-time diversification, cryptography, OS interface scrambling) 6. On Metrics - how do we even define and measure a bug? ("There are far too many proposed measures to evaluate or even list here. We can state that, as alluded to above, metrics and measures should be firmly based on well-established science and have a rational foundation in metrology to have the greatest utility.") Government Calls to Action: 1. Engage the research community (funding, contests and prizes, infrastructure) 2. Education & training for the dev community (school curriculum, training programs) 3. Policy, Legal, etc. (procurement standards, liability for failures, insurance, standards, code repositories) --- In my opinion, this is a good piece to skim through as you'll probably come across 1 or 2 practices/fields you hadn't heard of before. The recommendations are (intentionally) vague. Functional security is already taken very seriously in many life and safety-critical industries. One potentially-troubling trend we are seeing in the automotive/aerospace & defense industry is the consolidation of traditionally disparate systems into heterogeneous, multicore processors in order to save on hardware costs. These systems are relatively complex, and have the potential to mix safety-critical environments (brakes, steering, acceleration ECUs running an RTOS) with application environments (infotainment system running Linux). Partitioning is big here. There are well-defined and accepted standards for the majority of industrial automation, transportation, medical, automotive, and aerospace & defense targeted systems. Data security and privacy is not taken seriously by the majority of consumer corporations (and even some government agencies), and won't be until the legal repercussions of failing to protect client information are a serious threat to the companies that build and maintain these databases and systems.
gwu78 10y ago
Of the many recurring stupid ideas for startups I have had is a software company that does not write code. Instead it edits and removes code. This has been called "negative coding." Few people write small programs anymore. UNIX, the OS that runs the internet and on which the "cloud" depends, is a time-capsule full of small programs. What this might mean is left as an exercise for the reader. Today, large programs are celebrated without question. Gratuitous complexity can be disguised as "productivity" and pitched as value creation. At the very least it can be a source of fascination for futurists. Any liabilities created in the process can be easily explained away. Among the many things that can be done with this output, one of them to is to make small programs from the larger ones. As far as I can tell, this is not being done. For myself, I have taken large, open source programs and gutted all the needless features in order to produce the small programs I want. My goal is less complexity. Simplicity is a loaded term. For myself, this process of incrementally reducing complexity "creates value". It is an intellectual exercise, there is a sense of productivity, and yet almost no code is written. Software companies are full of developers who cut, paste and compile. Today many of them are working with open sourced code. The software company I aim to start is comprised of "programmers" who also work with such open sourced code, they only cut and compile. EDIT: Whenever I see the "Who's hiring" thread I always wish I could put in an entry for this. The vision I have is a group of "early employees" with day jobs. Absent connections and name dropping no VC would ever fund this. No one will be paid to do this "negative coding" work until we secure our first government or Fortune 100 contract and they see the results. And even then I could not guarantee the results would be appropriately valued. But were this fictional company to succeed, those early employees could claim they were an integral part of a monumental paradigm shift. EDIT 2: The fictional company does negative coding on single programs to reduce them in size or to break them up into smaller programs and is not limited to the embedded market or driven by resource constraints. Selecting parts of an open source OS distribution to create a new distribution is a different idea and of course many companies have been doing that for many years.
- usgroup 10y ago
  Shut up and take my money! :)
hyperion2010 10y ago
I find this hilarious in light of what we know about the NSA. All solid recommendations, but they are bandaids when compared to the sheer weight of capital that is being misused by hoarding known vulns. Unfunded mandates are fine for grandstanding.
- schoen 10y ago
  I strongly oppose vulnerability hoarding, but I'd point out that if we don't think it's easy to make political or cultural progress against it quickly, a technical alternative to make people safer is actually finding ways to make safe software. Plus, if "bugs are dense" advocates are right, we need major qualitative improvements to software development in order to make much of an impact (because they argue that different hoarders, or even different from-scratch researchers, would primarily know about different bugs). 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.
jwmullally 10y ago
They should have pasted this diagram all over the document: https://en.wikipedia.org/wiki/Automata_theory https://en.wikipedia.org/wiki/Automata_theory I'm disappointed that the "Formal Methods" section makes only a passing reference to Finite State Machines. FSMs are arguably the easiest to understand and use formal methodology, and probably the most prevalent. Especially worth emphasizing given how difficult and opaque a lot of formal methods remain to even people with 4 year CS bachelor degrees. This old thread https://news.ycombinator.com/item?id=2949543 https://news.ycombinator.com/item?id=2949543 had lots of interesting discussions on FSMs, particularly their current widespread use in (sometimes mission-critical) embedded systems. An ongoing problem seems to be a lack of robust first-class support for FSMs in every day programming languages, which can limit debugging, static analysis, standard tools etc. Disclaimer: I know nothing about security or formal methods.
- nickpsecurity 10y ago
  High-assurance security from 80's-90's used them too in both formal specifications and coding approach. It was more like looking at the kernel as a giant, state machine but you can do protocols or app components, too. Many will complain about unreadability of C code. However, a proper spec or DSL for state machines makes them extremely readable with the C code autogenerated. They're also extremely easy to formally verify as you pointed out. 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/publications/the-next-wave/assets/files/TNW-19-1.pdf https://www.nsa.gov/resources/everyone/digital-media-center/...
  - nitrogen 10y ago
    If each state is a function that simply waits for events and returns the next state, the C code doesn't look that bad.
    - nickpsecurity 10y ago
      It doesn't look bad versus regular C. You still have the C-specific risks in the module and at module interfaces that other language reduce. It's also harder to parse, analyze, and compile in a secure way. With SPARK & formal tools, one can get a strong analysis that the code will always meet the spec. The ability to fully do that for C has only come online in the past few years. It appears to take more work, too.
nickpeterson 10y ago
My affection for F# likes that ML and F# are explicitly mentioned in section 3.4.2 "Better Code".
eganist 10y ago
Incidentally, BSIMM 7 (https://www.bsimm.com/download/ https://www.bsimm.com/download/) also came out this month. Whereas BSIMM is descriptive and OpenSAMM (http://www.opensamm.org/ http://www.opensamm.org/) is prescriptive, I'm curious to see how NIST tackles the secure development lifecycle.

132 points by Dowwie 10y ago

This is an interesting read. Despite this, I still cannot understand what a Formal Method is. 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.

adrianN 10y ago
Not exactly what you're looking for, but maybe a good starting point http://cs.stackexchange.com/questions/13785/formal-program-verification-in-practice http://cs.stackexchange.com/questions/13785/formal-program-v...
quantumhobbit 10y ago
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.
- johncolanduoni 10y ago
  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.
dwheeler 10y ago
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-Software-10-Formal-Methods.ppt 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/ 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.
- retox 10y ago
  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.
  - nickpsecurity 10y ago
    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-secure-software-an-invitation-to-ada-2012/ http://www.adacore.com/knowledge/technical-papers/safe-and-s...
- gravypod 10y ago
  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?
joshmarlow 10y ago
I'm about to start reading "The Little Prover" (https://mitpress.mit.edu/books/little-prover https://mitpress.mit.edu/books/little-prover) which sounds like a good intro.
- nickpsecurity 10y ago
  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.
tptacek 10y ago
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.
- alaithea 10y ago
  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/ https://github.com/opencontrol/compliance-masonry https://github.com/opencontrol/compliance-masonry
  - tptacek 10y ago
    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.
    - alaithea 10y ago
      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/ https://compliance.cloud.gov/ (<- all auto-gen, AFAIK)
jerf 10y ago
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.
nabla9 10y ago
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 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.
stonemetal 10y ago
A Formal Method means to create a Formal System and construct a formal proof. https://en.wikipedia.org/wiki/Formal_system 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 https://en.wikipedia.org/wiki/Hoare_logic
- gravypod 10y ago
  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.
  - vilhelm_s 10y ago
    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.)
agentultra 10y ago
> 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.
nickpsecurity 10y ago
Here's the two, best books on it that I know of that are available for free: http://adam.chlipala.net/cpdt/cpdt.pdf http://adam.chlipala.net/cpdt/cpdt.pdf https://www.cis.upenn.edu/~bcpierce/sf/current/index.html 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 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 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 http://www.dwheeler.com/essays/high-assurance-floss.html
udkl 10y ago
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/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/fo...
jk4930 10y ago
Recent article and discussion: https://news.ycombinator.com/item?id=12612856 https://news.ycombinator.com/item?id=12612856 (A Hoare Logic for Rust)

jefffoster 10y ago

I wonder if this'll (or something like it) be the tipping point for governments to introduce more regulations for software? We already have regulations like PCI-DSS for dealing with payment card, maybe this'll end up with regulations for dealing with security? The conclusion suggests better specification, better testing and more resilient architectures are the strategies that could make a difference. Perhaps software engineering will have to agree on a set of "best" practices that make security problems less likely to occur? (typos)

mildweed 10y ago
I can definitely see more standards and certifications coming to pass, which then later distill down to one or two primary certifications that everybody aspires to get. Currently there are multiple privacy/security standards (PCI, HIPPA, FERPA, etc). We'll probably have to get more opinions from more sensitive-data industries, and then for them all to find the common ground. 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."
- ryanmarsh 10y ago
  Regulatory enforcement. Even though PCI DSS is enforced by a private regulatory body, it still carries weight. HIPAA has HHS which does investigate and lead to corrective action. Both of these bodies scare the crap out of a lot of companies. I've worked in both sectors (banking/credit, healthcare) and the fear is palpable. If the CFPB had the ability to enforce regulatory requirements for handling of PII you bet your ass companies would fall in line. Nobody wants trouble with the feds.
  - schoen 10y ago

realkitkat 10y ago

Although it does mention some risks of using 3rd party code/components in passing under 'Understanding and Controlling Dependencies' (835-), I would have expected them to make a stronger case for OWASP 2013-TOP10-A09: 'using components with known vulnerabilities'[1] type of analysis. This applies to almost any kind of modern application, not just web apps, but especially to those written in native languages (C/C++/...) as we increasingly build our applications by bringing in varying amounts of 3rd party code; open source or commercial. Like traditional static code analysis, more or less mature tooling exists in open source[2][3][4] and commercial capacity to perform static binary and source code analysis to discover and track 'offending' 3rd party code, which does make it practical to include this kind of analysis to sdl/sdlc/devops workflows. [1] https://www.owasp.org/index.php/Top_10_2013-A9-Using_Components_with_Known_Vulnerabilities https://www.owasp.org/index.php/Top_10_2013-A9-Using_Compone... [2] http://www.binaryanalysis.org/en/home http://www.binaryanalysis.org/en/home [3] https://www.owasp.org/index.php/OWASP_Dependency_Check https://www.owasp.org/index.php/OWASP_Dependency_Check [4] https://github.com/OWASP/SafeNuGet https://github.com/OWASP/SafeNuGet

roymurdock 10y ago

Goal: The goal of this report is to present a list of specific approaches that have the potential to make a dramatic difference reducing vulnerabilities – by stopping them before they occur, by finding them before they are exploited or by reducing their impact. Impetus: In response to the February 2016 Federal Cybersecurity Research and Development Strategic Plan, NIST was asked to identify ways to dramatically reduce software vulnerabilities. NIST worked with the software assurance community to identify five promising approaches. This report presents some background for each of the approaches along a summary statement of the maturity of the approach and the rationale for why it might make a dramatic difference. Further reading was provided for each approach. Hopefully other approaches will be identified in the future. Current Cybersecurity Approaches: 1. Formal Methods - how do you check your program while writing code? (static analysis, model checkers, pragmas, model-based programming, and more recently contracts) 2. System Level Security - how do you partition components in a system? (containers/hypervisors/virtualization with smart API calls) 3. Additive Software Analysis - how do you analyze completed software to check for problems? (expression and exchange standards, better IDE plugins, advanced static analysis tools) 4. Mature Development Standards - how can you modify and reuse tried and tested code? (find, understand, learn, and combine the most relevant frameworks) 5. Moving Target Defense & Artificial Diversity - how can you minimize your program's attack surface? (compile-time diversification, cryptography, OS interface scrambling) 6. On Metrics - how do we even define and measure a bug? ("There are far too many proposed measures to evaluate or even list here. We can state that, as alluded to above, metrics and measures should be firmly based on well-established science and have a rational foundation in metrology to have the greatest utility.") Government Calls to Action: 1. Engage the research community (funding, contests and prizes, infrastructure) 2. Education & training for the dev community (school curriculum, training programs) 3. Policy, Legal, etc. (procurement standards, liability for failures, insurance, standards, code repositories) --- In my opinion, this is a good piece to skim through as you'll probably come across 1 or 2 practices/fields you hadn't heard of before. The recommendations are (intentionally) vague. Functional security is already taken very seriously in many life and safety-critical industries. One potentially-troubling trend we are seeing in the automotive/aerospace & defense industry is the consolidation of traditionally disparate systems into heterogeneous, multicore processors in order to save on hardware costs. These systems are relatively complex, and have the potential to mix safety-critical environments (brakes, steering, acceleration ECUs running an RTOS) with application environments (infotainment system running Linux). Partitioning is big here. There are well-defined and accepted standards for the majority of industrial automation, transportation, medical, automotive, and aerospace & defense targeted systems. Data security and privacy is not taken seriously by the majority of consumer corporations (and even some government agencies), and won't be until the legal repercussions of failing to protect client information are a serious threat to the companies that build and maintain these databases and systems.

gwu78 10y ago

Of the many recurring stupid ideas for startups I have had is a software company that does not write code. Instead it edits and removes code. This has been called "negative coding." Few people write small programs anymore. UNIX, the OS that runs the internet and on which the "cloud" depends, is a time-capsule full of small programs. What this might mean is left as an exercise for the reader. Today, large programs are celebrated without question. Gratuitous complexity can be disguised as "productivity" and pitched as value creation. At the very least it can be a source of fascination for futurists. Any liabilities created in the process can be easily explained away. Among the many things that can be done with this output, one of them to is to make small programs from the larger ones. As far as I can tell, this is not being done. For myself, I have taken large, open source programs and gutted all the needless features in order to produce the small programs I want. My goal is less complexity. Simplicity is a loaded term. For myself, this process of incrementally reducing complexity "creates value". It is an intellectual exercise, there is a sense of productivity, and yet almost no code is written. Software companies are full of developers who cut, paste and compile. Today many of them are working with open sourced code. The software company I aim to start is comprised of "programmers" who also work with such open sourced code, they only cut and compile. EDIT: Whenever I see the "Who's hiring" thread I always wish I could put in an entry for this. The vision I have is a group of "early employees" with day jobs. Absent connections and name dropping no VC would ever fund this. No one will be paid to do this "negative coding" work until we secure our first government or Fortune 100 contract and they see the results. And even then I could not guarantee the results would be appropriately valued. But were this fictional company to succeed, those early employees could claim they were an integral part of a monumental paradigm shift. EDIT 2: The fictional company does negative coding on single programs to reduce them in size or to break them up into smaller programs and is not limited to the embedded market or driven by resource constraints. Selecting parts of an open source OS distribution to create a new distribution is a different idea and of course many companies have been doing that for many years.

usgroup 10y ago
Shut up and take my money! :)

hyperion2010 10y ago

I find this hilarious in light of what we know about the NSA. All solid recommendations, but they are bandaids when compared to the sheer weight of capital that is being misused by hoarding known vulns. Unfunded mandates are fine for grandstanding.

schoen 10y ago
I strongly oppose vulnerability hoarding, but I'd point out that if we don't think it's easy to make political or cultural progress against it quickly, a technical alternative to make people safer is actually finding ways to make safe software. Plus, if "bugs are dense" advocates are right, we need major qualitative improvements to software development in order to make much of an impact (because they argue that different hoarders, or even different from-scratch researchers, would primarily know about different bugs). 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.

jwmullally 10y ago

They should have pasted this diagram all over the document: https://en.wikipedia.org/wiki/Automata_theory https://en.wikipedia.org/wiki/Automata_theory I'm disappointed that the "Formal Methods" section makes only a passing reference to Finite State Machines. FSMs are arguably the easiest to understand and use formal methodology, and probably the most prevalent. Especially worth emphasizing given how difficult and opaque a lot of formal methods remain to even people with 4 year CS bachelor degrees. This old thread https://news.ycombinator.com/item?id=2949543 https://news.ycombinator.com/item?id=2949543 had lots of interesting discussions on FSMs, particularly their current widespread use in (sometimes mission-critical) embedded systems. An ongoing problem seems to be a lack of robust first-class support for FSMs in every day programming languages, which can limit debugging, static analysis, standard tools etc. Disclaimer: I know nothing about security or formal methods.

nickpsecurity 10y ago
High-assurance security from 80's-90's used them too in both formal specifications and coding approach. It was more like looking at the kernel as a giant, state machine but you can do protocols or app components, too. Many will complain about unreadability of C code. However, a proper spec or DSL for state machines makes them extremely readable with the C code autogenerated. They're also extremely easy to formally verify as you pointed out. 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/publications/the-next-wave/assets/files/TNW-19-1.pdf https://www.nsa.gov/resources/everyone/digital-media-center/...
- nitrogen 10y ago
  If each state is a function that simply waits for events and returns the next state, the C code doesn't look that bad.
  - nickpsecurity 10y ago
    It doesn't look bad versus regular C. You still have the C-specific risks in the module and at module interfaces that other language reduce. It's also harder to parse, analyze, and compile in a secure way. With SPARK & formal tools, one can get a strong analysis that the code will always meet the spec. The ability to fully do that for C has only come online in the past few years. It appears to take more work, too.

nickpeterson 10y ago

My affection for F# likes that ML and F# are explicitly mentioned in section 3.4.2 "Better Code".

eganist 10y ago

Incidentally, BSIMM 7 (https://www.bsimm.com/download/ https://www.bsimm.com/download/) also came out this month. Whereas BSIMM is descriptive and OpenSAMM (http://www.opensamm.org/ http://www.opensamm.org/) is prescriptive, I'm curious to see how NIST tackles the secure development lifecycle.