13 ms·

Hacker-Proof Code Confirmed

147 points by sprucely 10y ago

jeyoor 10y ago
I think rigorous application of formal methods plus deployment techniques like unikernels have the potential to improve the quality of a lot of software.
- hprotagonist 10y ago
  now if we could only figure out how to make Coq for parallel or asynchronous routines...
  - bahjoite 10y ago
    Would TLA be of any help to you? https://research.microsoft.com/en-us/um/people/lamport/tla/tla.html https://research.microsoft.com/en-us/um/people/lamport/tla/t...
  - felixgallo 10y ago
    All data is immutable, and there is no message passing. Done!
- __jal 10y ago
  I'm more of a pessimist. If you can't get C programmers to handle memory buffers correctly, how are you going to get them to use actual formal methods or annotations that rely on understanding substantially more math than the average programmer has?
  - kordless 10y ago
    Make the infrastructure you run things on provide what appears to be formal methods for interactions, but also make it appear inconsistent over a given regular timeframe. Abusers of the system will find lots of issues with it because it will break unpredictably at random times if they are hammering away. Happy users of the system will having it break every now and again, but will likely avoid making things overly complex as a result of it increasing the chances it will break over a given time period. Expecting infrastructure to be completely reliable is a fallacy and should be embraced instead of chased. Suffering on the part of the former "programmer" (hacker) will be paid while obtaining results of various runs to exploit the system from the outside (external). Suffering on the part of the later "programmer" (coder) will be paid internally while working on more efficient solutions. We'll need to code up the two types of suffering into stores of value, and tie them to cryptocurrencies, but that should be fairly straightforward to implement.
  - nickpsecurity 10y ago
    People learned 4GL's, BASIC, Scratch, COBOL, etc pretty easy. That means the solution is make it higher-level with the compiler, type system, protocol generators, etc doing most of the work. They just need a set of tools that let them express themselves in a way constrained enough to let the tooling produce correct code. Eiffel and Ada/SPARK results are also very promising on systematically eliminating errors from large applications. Experienced users will be able to do more than the basic 4GL or whatever.
codemac 10y ago
Has anyone successfully brought formal methods to an area of code that is newly being developed? I have successfully convinced management to allow me to use formal methods on portions of very old code (~17 years old at the time) that are being rewritten.. but I've never been able to get management on board with the time required for new development with formal methods. The planning time up-front is more than what a lot of companies are willing to tradeoff for time-to-market.
- Ben-G 10y ago
  Amazon has made use of formal methods during the development of AWS. Relevant paper can be found here: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/abstract http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-s...
  - codemac 10y ago
    Found a much better link :) 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...
- fredyr 10y ago
  I'd be very interested if you could elaborate a little on what tools and how you applied formal methods on that old code?
lazaroclapp 10y ago
Quick reminder that verified code is only hacker-proof provided that: a) The specification correctly describes all correct behavior and correctly proscribes all incorrect behavior (basically, you trade a huge codebase for a smaller one in the form of the spec, which is a massive improvement, but as long as humans write the spec it is not clear it can ever be fully hacker-proof) b) The trusted computing base works as modeled in the spec. Even on the limit, that means that the physical properties of the hardware are as we expect them to be and that our understanding of the laws of physics is correct. Slightly below this threshold there are things like Row Hammer attacks (https://en.wikipedia.org/wiki/Row_hammer https://en.wikipedia.org/wiki/Row_hammer ). Before even this: microcode bugs, proof-verifier bugs, etc. That said, formal methods do provide a huge improvement over the state of the art of completely unspecified software, and have been shown to work in practice to greatly reduce the number of vulnerabilities of important large systems such as compilers, kernels and now remote controlled helicopters. They might not be appropriate for every piece of software quite yet, but I would greatly like to see this stuff for things like self-driving cars, airplane autopilots, smart grids and smart factories and in general all of the rapidly approaching "heavy" IoT applications. Also, some verified properties of commodity OS would be very nice to have (say container isolation in a cloud environment or non-leaking of keys for a smart wallet process).
- andrewchambers 10y ago
  > basically, you trade a huge codebase for a smaller one in the form of the spec Most formally verified things i have seen require huge amounts of 'spec' code compared to the implementation.
  - microcolonel 10y ago
    You're confusing the specification with the equivalence proof. A spec is likely going to be about as simple as an implementation, with the benefit that it can be read more consistently.
    - adrianN 10y ago
      All the specs for real world things I've seen are long and use fuzzy language. Making them formal enough to provide a basis for verification will only make them longer.
tracker1 10y ago
I think the biggest issue is from a business people perspective, formal requirements needed for this type of development (software development as an engineering discipline) is too slow, and not as open to change as the agile (craft) methods tend to be in software.
- saretired 10y ago
  It depends what business you're in and what your needs are. Agile doesn't get much traction in flight control software or telephone switches.
  - tracker1 10y ago
    Exactly... anything dealing with critical hardware will/should be done as an engineering discipline wrt development, where tfa's practices could be better. That isn't the majority of software development, which is one-off line of business apps.
heimatau 10y ago
To save others time. I've copied some of the biggest points of the article. My comments are in [brackets], except these^^ first few sentences. "Between the lines it takes to write both the specification and the extra annotations needed to help the programming software reason about the code, a program that includes its formal verification information can be five times as long as a traditional program that was written to achieve the same end." "Jeannette Wing, corporate vice president at Microsoft Research. “Any natural language is inherently ambiguous. In a formal specification you’re writing down a precise specification based on mathematics to explain what it is you want the program to do.”" "“We’re not claiming we’re going to prove an entire system is correct, 100 percent reliable in every bit, down to the circuit level,” Wing said. “That’s ridiculous to make those claims. We are much more clear about what we can and cannot do.”" [In the experiment the article is mostly based on] "The hackers were mathematically guaranteed to get stuck. “They proved in a machine-checked way that the Red Team would not be able to break out of the partition, so it’s not surprising” that they couldn’t, Fisher said. “It’s consistent with the theorem, but it’s good to check.”" "In a return to the spirit that animated early verification efforts in the 1970s, the DeepSpec collaboration led by Appel (who also worked on HACMS) is attempting to build a fully verified end-to-end system like a web server. If successful, the effort, which is funded by a $10 million grant from the National Science Foundation, would stitch together many of the smaller-scale verification successes of the last decade. Researchers have built a number of provably secure components, such as the core, or kernel, of an operating system. “What hadn’t been done, and is the challenge DeepSpec is focusing on, is how to connect those components together at specification interfaces,” Appel said."
- mkstowegnv 10y ago
  "Jeannette Wing, corporate vice president at Microsoft Research. “Any natural language is inherently ambiguous." Lojban (nee Loglan) is a conlang designed to be syntactically unambiguous but as usable in speech and thought as a natural language https://en.m.wikipedia.org/wiki/Lojban_grammar https://en.m.wikipedia.org/wiki/Lojban_grammar
alexchantavy 10y ago
> “We’re not claiming we’re going to prove an entire system is correct, 100 percent reliable in every bit, down to the circuit level,” Wing said. “That’s ridiculous to make those claims. We are much more clear about what we can and cannot do.” This is an important statement that should be highlighted more prominently in the article (whose title I disagree with). Formal methods are promising, and I'm glad that the researcher acknowledged that when your project relies on so many other abstractions and systems it doesn't matter how rigorously developed your solution is if a hacker can find a way to accomplish their objective through one of your dependencies.
- rocqua 10y ago
  Specifically, hardware level exploits are wholly disregarded by formal verification. This means bit-banging could still work. In many systems I'd also be wary of the OS itself.
  - nickpsecurity 10y ago
    They're disregarded by software verification. There's more formal verification deployed in hardware than software. There's also techniques to verify hardware and software together. The hardware problems you see are often deliberately left in there either due to corner cutting or backward compatibility with bad designs of the past. Both inspired by desire to see the number next to net income continue to rise. ;)
eriknstr 10y ago
I Google'd HACMS project and found an Open Catalog page at DARPA with a bunch of links to open source software and paper PDFs. Seem worth checking out to anyone whose interest was piqued by the article. http://opencatalog.darpa.mil/HACMS.html http://opencatalog.darpa.mil/HACMS.html
kelvin0 10y ago
A while back I was exploring the use of 'soft' formal methods to help in evaluating correctness of some new modules we had to develop. I had come upon Alloy, which seems like a gentler introduction to formal methods (Unlike Z or Coq). http://alloy.mit.edu/alloy/ http://alloy.mit.edu/alloy/ Anyone have any experience using Alloy, or some other formal method?
- maramono 10y ago
  I've used it several times but the big problem with it is that once you have a nice, correct model that has been checked (and no counterexamples found), there's no way to translate it to code. This meand that your basically back on square one in terms of implementation. I really like (and use quite often) the ASM method instead. More of my thoughts here: http://ortask.com/how-i-designed-built-and-tested-a-temperature-logger-with-arduino-part-2/ http://ortask.com/how-i-designed-built-and-tested-a-temperat...
  - nickpsecurity 10y ago
    There's actually been imperative extensions and prolog compilers for it. Here you go: https://homes.cs.washington.edu/~emina/pubs/alloy.mscs13.pdf https://homes.cs.washington.edu/~emina/pubs/alloy.mscs13.pdf Also, for ASM's, the most interesting one I've seen is certified compiler project that is taking a lot less lines of code than CompCert: https://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf https://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf
phantom_oracle 10y ago
Here are my questions (to anybody with knowledge of this field): - Is this type of programming related to the functional-programming field? - How is this different to OOP/imperative code? - What language(s) will be used to write code for this?
- AstralStorm 10y ago
  I can speak about Isabelle/HOL specifically only. 1) functional programming is a subset of mathematical proofs. Isabelle syntax is somewhat similar to what is offered in ML family of functional languages. Unlike functional languages, you can use more advanced constructs than bijections (can model superposition etc.) and it is easier to state things over sets. 2) imperative code is a subset to this too with added order of operations. Language is somewhat different though Isabelle has a module that has necessary proofs to verify imperative programs.
acfoltzer 10y ago
I'm one of the researchers at Galois who's working on the quadcopter platform for HACMS. Let me first say that this headline makes me cringe just as much as anyone. I'd also like to give folks a pointer to some of the work we've developed on the project–it's all open source. First we have Ivory, the DSL for doing safe systems programming that takes buffer overflows and other memory-safety bugs off the table: http://ivorylang.org/ http://ivorylang.org/ [1] Second, the flight control software we wrote for the 3DR Iris+: http://smaccmpilot.org/ http://smaccmpilot.org/ The adventurous among you who fly with a Pixhawk can build it and try it out yourselves, and we'd love to hear your thoughts. [1]: When we began work on HACMS, Rust was around but nowhere near mature enough to base a proposal on. These days, it covers a lot of the same bases, although currently Ivory is more suited for formal analysis with SMT solvers and model checkers.
- eggy 10y ago
  Glad to hear you say that. Aside from that the work seems very interesting. I am going to check out Ivory. I have been reading up and playing with Idris and F. I like F so far, and that you can output F# and OCaml. Idris's goals seem in line with what you were originally looking for. Have you evaluated it?
  - eggy 10y ago
    [Edit] Replying to my post to edit, since no choice given to edit. Should say "I like Fstar" above, but asterisk turned on italics...
  - acfoltzer 10y ago
    Indeed, we're fans of Idris here, and even hosted a series of Idris tech talks: https://galois.com/blog/2015/01/tech-talk-dependently-typed-functional-programming-idris-1-3/ https://galois.com/blog/2015/01/tech-talk-dependently-typed-... The goals of Idris and similar languages are different from the goals we had with Ivory, though. We sometimes describe Ivory as "medium-assurance" as opposed to the high assurance one can get from a language with a more expressive type system. It makes sense for some systems or components to be formally verified, for example the seL4 verified microkernel which is also used on our copter. However we simply would not have been able to formally verify (or even get to typecheck with fancier dependent types) something on the scale of an autopilot given the resources we had on the project. Instead we rely on getting quite a bit of bang for the buck with the memory safety features, and then augment with assertions. We ended up with a working autopilot (and board-support package with drivers) in only ~4 engineer-years, so we think the tradeoff is working well so far :)
mirceal 10y ago
For anybody interested in this field: Specifying Systems by Leslie Lamport, the same guy that gave us Logical Clocks and Paxos (free on Ms Reseach website): http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/bo...
neilellis 10y ago
This article was just wildly misleading, the title is well, it speaks for itself. Interesting language and rather than 'formally proven' as the article wildly claims it is a strongly typed system ala Haskell. So yep looks a great idea for secure systems - but formally proven - bah! :-) Has anyone here actually formally proved a non trivial program, say a couple of hundred lines on NCSS? How about tens of thousands, hundreds of thousands or millions of lines of code. The complexity of the proof would be insanely complicated such that the level of expertise to define the requirements would be (if at all within the limits of human endeavour) only for maybe a handful of people. And do those people make good business analysts, or hackers, or entrepreneurs or even just communicators. Jeez the misinformation that gets spread!
- tzs 10y ago
  > Has anyone here actually formally proved a non trivial program, say a couple of hundred lines on NCSS? I don't know what NCSS is, so am going to answer as if your sentence stopped two words earlier. How about the CompCert C compiler [1]? Or CakeML [2]? And let's not forget seL4 [3], which has a formal proof that the implementation in C conforms to the specification, and a further formal proof that the binary code is a correct translation of the C code. [1] http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html [2] https://cakeml.org https://cakeml.org [3] https://sel4.systems https://sel4.systems
bikamonki 10y ago
Just thinking out loud: if a program can check the correctness of another program against a formal spec, can't it just write the checked program from the spec?
- dougws 10y ago
  You've just invented the field of program synthesis, which is a super active research area right now in programming languages! Here's the paper list from a class at UW focused on this area: http://courses.cs.washington.edu/courses/cse599a2/15wi/ http://courses.cs.washington.edu/courses/cse599a2/15wi/ . The Sumit Gulwani paper from the first week is a really good introduction to the field.
- derkha 10y ago
  Aside from program synthesis, there is the more restricted form of code extraction, which turns definitions inside a theorem prover into code in a more traditional, runnable language such as OCaml. But you'll still want to do one or more refinement steps inside the theorem prover where you turn your spec into more efficient definitions (or even definitions that are computable at all - how do you evaluate an unbounded universal quantifier?)
- stale2002 10y ago
  Well then the spec isn't just a spec. It is a programming language in and of itself. And how do you prove that THAT spec is correct? It is turtle specs all the way down.
  - Crespyl 10y ago
    Sooner or later your spec language is just English and you have to get the lawyers involved. ;)
- usgroup 10y ago
  Have a look at Why3 for example or Coq. That's exactly what formal verification systems do: 1. Formally prove intention. 2. Generate code.
- 10y ago
walter_bishop 10y ago
Such 'hacker-proof code' can only be as secure as the underlying hardware. If such a cure already existed, we wouldn't be subjected to the current hacking/phishing epidemic. "these malfunctions could be as simple as a buffer overflow" No amount of 'formal verification' will detect or prevent buffer overflows, which are a defect in how the hardware allocates memory. The cure must also be found in the hardware. "Back in the 20th century, if a program had a bug, that was bad, the program might crash, so be it,” It must of been on a different planet, cause I can remember using networked computers in college way back in 1984. and the first Internet worm occurred in 1988.
- marcoperaza 10y ago
  Hardware bugs are NOT the major source of widely-exploited vulnerabilities in practice. They're a tiny fraction of exploits being used in the wild, and certainly of the ones being used to target the general population. Further, a buffer overflow is absolutely not a defect in how hardware allocates memory. It's a logical flaw in the software that reads/writes beyond the limits of the memory the programmer intended to access.
  - mistaken 10y ago
    It's also worth noting that some critical hardware components (e.g. CPUs since the infamous division bug) are formally verified as well, so manufacturing defects should be the largest concern for them.
    - AstralStorm 10y ago
      Only a tiny fraction of the CPU is formally verified. There are frequent errata. And plenty of undefined behaviour as well as races you can hit if you really try.
peterbonney 10y ago
Aside from the obvious point that software can obly be as secure as the hardware it runs on, isn't Gödel's incompleteness theorem a problem with scaling from smallish problems to biggish ones? Granted it has been a long time since I understood it even moderately well, but my main recollection is that a complete system of logic can't be consistent, and a consistent system can't be complete. That would seem to be an issue with extending formal methods to any computer system of broad general use. Or am I misapplying the theorem here?
- Jweb_Guru 10y ago
  Static type systems were explicitly designed to get around various inconsistency problems with standard formulations of mathematics (ZFC, etc.). Formal verification generally exploits such type systems. In a nutshell, the incompleteness theorem (and related problems) only apply to sufficiently powerful logical systems (namely, those that can model Robinson arithmetic). Less powerful (or, in some cases, incomparable) axiom schemes exist that are capable of being both consistent and complete. Usually, the cost is that (1) they are not capable of expressing all programs (but many people argue that they are capable of expressing all useful programs), and (2) some programs that are correct in those type systems may require exponentially larger proofs (types) than a less stringent system would require in order to accept the same term (again, many people argue that this does not matter in practice).
  - peterbonney 10y ago
    Also interesting - thank you.
- MrManatee 10y ago
  Gödel's incompleteness theorems are more of a theoretical limitation than a practical one. Roughly speaking, Gödel's incompleteness theorems say that all proof systems for number theory are limited in some way. For example, first-order Peano arithmetic is such a system, and one of its limitations is that it doesn't support transfinite induction. (It doesn't matter if you don't know what it is.) In other words, if you want to translate a mathematical proof to Peano arithmetic, you have to come up with a way to do it without transfinite induction. Sometimes, such in the case of Goodstein's theorem, this is impossible. To prove Goodstein's theorem, you have to choose a stronger proof system to begin with. So, Gödel's theorems guarantee that no matter how strong you proof system is, there are always number-theoretic statements that are beyond its reach. But for reasons that are not currently completely understood, this doesn't really happen in practice. "Naturally occurring" examples of number-theoretic statements almost always turn out to be provable in surprisingly weak systems. Instead, you run into practical problems: the theorem is provable in the system, but actually writing out the proof is utterly inconvenient. As an analogy, there are Turing-complete programming languages that don't have the concept of functions. In theory, they are capable of all kinds of computations, but in practice you don't want to use them. And if, instead of mathematics, we concentrate on proofs of correctness, then this is even less of a practical problem. To quote Leslie Lamport, proofs of correctness "are seldom deep, but usually have considerable detail." The proofs may be long and complicated, but as long as they don't use any kind of ridiculously abstract techniques, they are just the kind of proofs where computers can have an advantage over humans.
jopaki 10y ago
This is the right topic people. This is what needs to get into mainstream narratives of malware/vulns.
gravypod 10y ago
I don't get the idea of a formal method. You're attempting to prevent bugs in code by writing code that describes the final product. In any reasonably complex system the descriptions will be large, complex, and bug prone. How is a "formal method" any better then one of the following: - Unit testing: Provide every test case possible - Pure Functions: Use small methods that cannot error and always return sane values - Fuzzing Testing: To find if the implementation is actually correct or if it is correct by chance What is the benefit of a formal method? It's just inconceivable for me to see "Hacker-Proof code" and not laugh at whoever wrote this.
- SolarNet 10y ago
  Formal verification is a bit like using a super high level strict/static/safe programming language (often in conjunction with a classic programming language providing the actual run-time description which is being formally checked). Think C# attributes or python decorators but where they take up 80% of the code and are a language onto themselves. It basically does all of the things you described in your list through automatic formal mathematical proofs, rather than relying on chance or on the programmer directly (obviously if you write a backdoor into a formal requirement it'll make it past the proving step). - No need to unit test specific cases when all the cases have been formally proven. - Formal proving methods typically work best (or at least most easily) on pure functions for the reasons you described. - No need to fuzz random values when the entire range has been formally proven. If you ever took a theoretical computer science where the teacher had you write the formal induction proof for a loop, it's like that, where every possible case must be covered mathematically. We've simply gotten the computer to deduce the proofs for us automatically. For example if there is a global integer that can be between 0 and 700, or the value 1000, then the formal verification system will make sure nothing in the program can write any other value to that memory. It will never increment or decrement when a 1000 is in there, it will never subtract 20 when a value less than 20 is in there, etc. Including by buffer overflows, or by pointer arithmetic in some random function, or by a runaway parsing algorithm. And then we do that for ever piece of memory, every subroutine call, and every possible input. And then we prove we covered every case and never violated our spec. And we can add implications to our spec. For example the only way a command to launch a missile can happen is if the launch missile function is called, no other function no matter the state of the program can cause it to happen. This can prove that there aren't exploits to a complex program that might cause unwanted behavior. Can you prove that sort of thing to me about your software? Like can you prove to me your software is unbreakable? This solution can (with a much smaller error rate than "well I tried 17 things and none of them worked." because it can say "I tried literally every possible thing."). It's a proactive solution. We are proving that it's mathematically impossible to break (engineering still being the weak point). That's an order of magnitude, if not more, better than what we have now.
TwoBit 10y ago
All we need now is a proof that the proof program is correct. And a proof that the proof proving program is correct.
- pka 10y ago
  Exactly :) And a proof that the spec is correct. But without formal verification both your spec and the implementation may be incorrect.
- AstralStorm 10y ago
  Internal consistency is relatively easy to verify. Completeness to some extent as well. The manual task is to verify all the assumptions.
Mao_Zedang 10y ago
I have always been interested in this area of programming. One thing I have always wanted is the ability to enforce restrictions on data types beyond memory. By that I mean say i am using an int, what if I want to restrict this to actually 1 -55 you can solve this using run time error handling but wouldnt it be better if we had static checks where upstream we could see an unbounded int being passed into this method and throw a compile error.
- manmal 10y ago
  I think you could do that, but as long as you allow the usual operations on bounded variables (say, multiplication), you would have to ensure that the other operand is also bounded, or else you get an unbounded result nonetheless. Meaning, all variables that are used in any expression would have to be bounded eventually. There's also the problem that the compiler would have to infer that [1-10] - [1-2] can be negative, but does not have to. So with every expression on bounded variables, you increase their bounds' range, likely deleting the system's benefits.
  - Mao_Zedang 10y ago
    I agree its super complex, these bounds wouldn't be limited to integer based variables. I would also argue there are very narrow instances where you would want to bound a variable and also do arithmetic on it. The language should make the bounding optional and unbounded possible.
- tome 10y ago
  Check the liquid type of digitsP here: http://conscientiousprogrammer.com/blog/2015/12/23/24-days-of-hackage-2015-day-23-liquid-haskell-refinement-types-for-the-real-world/ http://conscientiousprogrammer.com/blog/2015/12/23/24-days-o...
eggy 10y ago
This is a big win for Haskell, since government contracts and approved vendors tend to have long arcs of doing future business. The idea an EDSL in Haskell was used greases the skids for any future Haskell acceptance on jobs. Good luck!
TickleSteve 10y ago
Although good, hasn't this just shifted the burden up a level? With formal methods, we can get proven-ish correct implementation, now we need bug-free specifications.... this in itself will be the next challenge. In the real world, specifications are very incomplete and fuzzy, partly because the business-level specifications are also fuzzy. This will not be a panacea, its simply shifted the burden up to a (possibly more manageable) level.
- nickpsecurity 10y ago
  "With formal methods, we can get proven-ish correct implementation, now we need bug-free specifications.... this in itself will be the next challenge." That's much better. See, before you needed to (a) understand a vague specification, (b) get your concrete version of it right, and (c) implement that specification. Now, you just trust a precise specification. That it's precise, esp if in Z or something, let's you check it against the people giving you vague stuff too by asking them questions. Solves lots of problems. Altran/Praxis Correct-by-Construction provides an illustration of how that works: http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf At another extreme, some companies capture requirements in formal logic then just compile them to code with logic programming languages like Mercury: http://www.missioncriticalit.com/development.html http://www.missioncriticalit.com/development.html Note: Not sure how well the last one works but worth mentioning that it's at least possible to go from specs to code in some places.
usgroup 10y ago
You might regard unit tests and formal proof to be opposite ends of the same scale with model driven testing being somewhere in between. One may be well advised to pick according to what you need. Formally proving the behaviour of your whole web app would likely take you an order of magnitude longer to write.
jbb555 10y ago
I don't understand this. In order to use formal verification you have to provide a complete and correct specification of what you want the software to do. We already have formal languages for doing this called programming languages. How is this any different from a programming language?
- danpalmer 10y ago
  Programming languages range in their formality. At the low end you have things like Python or Ruby, where you can write a loop over a type that can't be iterated, and it will crash at that line of code. In the middle you have languages like Java, C#, at the mid-high end, even Haskell and F#. In these languages they enforce type safety at varying levels throughout the code, by first inferring the types at each point throughout the code, and then seeing whether they are consistent. You would not be able to loop over a non-iterable object here. At the really high end you get into the realm of languages like Idris, Agda, and Ivory, and "formal verification" techniques. At this level you can not just write a loop, but you can write a loop that it is possible to prove terminates regardless of the input to the loop. This is done by setting constraints, and proving those constraints all the way through the code - the compiler will infer a lot of this, but it is still more work. This is a very simplified view of it, but essentially the more formal you get in the specification, the less chance that the program can do something unintentional, crash, or be hacked. The vast majority of the code written today is not that formally specified.
- fmap 10y ago
  Programming languages have to be (efficiently) executable, specifications can be logical/declarative. E.g. in a specification I can state things like "forall functions, with uncomputable property foo, we have bar". Plenty of things are uncomputable (e.g. quantifiers over natural numbers), but useful in specifications. There are good and bad specifications, same as for programs. For the semantics of a programming language you could essentially transcribe an interpreter in the form of a structural operational semantics and these are relatively error prone. Instead, you could give an axiomatic semantics, which is a lot more high-level. An equivalence proof between the two gives you a high level of assurance that the operational interpretation you had in mind while writing your interpreter actually means what you think it means. A recent example, the formal specification of the weak memory model of C11 turned out to be wrong (in the sense that it forbids common compiler optimizations, because programs have access to a time machine), but this was discovered when trying to develop a program logic for C11. In practice, most broken specifications I have seen were written by people who never really worked in formal verification. I am not aware of a single instance where a piece of formally verified code was broken because of a broken specification. There are cases where the specification had to be extended. E.g. CompCert was initially developed as a whole program compiler and the spec had to be extended for separate compilation. This broke the alias analysis.
virgulino 10y ago
"Beware of bugs in the above code; I have only proved it correct, not tried it." (Donald Knuth)
- AstralStorm 10y ago
  Statement hopefully obviated by seL4 Isabelle to/from C compiler.
lordnacho 10y ago
Can we get an actual example of a formally verified piece of code? If I have a function adding a and b, how does it look when it's "formally verified"?
- nickpsecurity 10y ago
  Good news is that most of them abstract the stuff away for common operations. They'll let you annotate code that's transformed into a set of verification conditions that the prover automatically discharges. SPARK is an example: http://www.skein-hash.info/SPARKSkein-release http://www.skein-hash.info/SPARKSkein-release Let's say that work isn't done. Then you have to hand model the properties of what you're doing. Arithmetic, expressed in bits, is harder than it appears to describe in a way that covers all the properties. Here's one on SmartMIPS: https://staff.aist.go.jp/reynald.affeldt/documents/affeldt-jssst2006-en.pdf https://staff.aist.go.jp/reynald.affeldt/documents/affeldt-j...

147 points by sprucely 10y ago

I think rigorous application of formal methods plus deployment techniques like unikernels have the potential to improve the quality of a lot of software.

hprotagonist 10y ago
now if we could only figure out how to make Coq for parallel or asynchronous routines...
- bahjoite 10y ago
  Would TLA be of any help to you? https://research.microsoft.com/en-us/um/people/lamport/tla/tla.html https://research.microsoft.com/en-us/um/people/lamport/tla/t...
- felixgallo 10y ago
  All data is immutable, and there is no message passing. Done!
__jal 10y ago
I'm more of a pessimist. If you can't get C programmers to handle memory buffers correctly, how are you going to get them to use actual formal methods or annotations that rely on understanding substantially more math than the average programmer has?
- kordless 10y ago
  Make the infrastructure you run things on provide what appears to be formal methods for interactions, but also make it appear inconsistent over a given regular timeframe. Abusers of the system will find lots of issues with it because it will break unpredictably at random times if they are hammering away. Happy users of the system will having it break every now and again, but will likely avoid making things overly complex as a result of it increasing the chances it will break over a given time period. Expecting infrastructure to be completely reliable is a fallacy and should be embraced instead of chased. Suffering on the part of the former "programmer" (hacker) will be paid while obtaining results of various runs to exploit the system from the outside (external). Suffering on the part of the later "programmer" (coder) will be paid internally while working on more efficient solutions. We'll need to code up the two types of suffering into stores of value, and tie them to cryptocurrencies, but that should be fairly straightforward to implement.
- nickpsecurity 10y ago
  People learned 4GL's, BASIC, Scratch, COBOL, etc pretty easy. That means the solution is make it higher-level with the compiler, type system, protocol generators, etc doing most of the work. They just need a set of tools that let them express themselves in a way constrained enough to let the tooling produce correct code. Eiffel and Ada/SPARK results are also very promising on systematically eliminating errors from large applications. Experienced users will be able to do more than the basic 4GL or whatever.

codemac 10y ago

Has anyone successfully brought formal methods to an area of code that is newly being developed? I have successfully convinced management to allow me to use formal methods on portions of very old code (~17 years old at the time) that are being rewritten.. but I've never been able to get management on board with the time required for new development with formal methods. The planning time up-front is more than what a lot of companies are willing to tradeoff for time-to-market.

Ben-G 10y ago
Amazon has made use of formal methods during the development of AWS. Relevant paper can be found here: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/abstract http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-s...
- codemac 10y ago
  Found a much better link :) 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...
fredyr 10y ago
I'd be very interested if you could elaborate a little on what tools and how you applied formal methods on that old code?

lazaroclapp 10y ago

Quick reminder that verified code is only hacker-proof provided that: a) The specification correctly describes all correct behavior and correctly proscribes all incorrect behavior (basically, you trade a huge codebase for a smaller one in the form of the spec, which is a massive improvement, but as long as humans write the spec it is not clear it can ever be fully hacker-proof) b) The trusted computing base works as modeled in the spec. Even on the limit, that means that the physical properties of the hardware are as we expect them to be and that our understanding of the laws of physics is correct. Slightly below this threshold there are things like Row Hammer attacks (https://en.wikipedia.org/wiki/Row_hammer https://en.wikipedia.org/wiki/Row_hammer ). Before even this: microcode bugs, proof-verifier bugs, etc. That said, formal methods do provide a huge improvement over the state of the art of completely unspecified software, and have been shown to work in practice to greatly reduce the number of vulnerabilities of important large systems such as compilers, kernels and now remote controlled helicopters. They might not be appropriate for every piece of software quite yet, but I would greatly like to see this stuff for things like self-driving cars, airplane autopilots, smart grids and smart factories and in general all of the rapidly approaching "heavy" IoT applications. Also, some verified properties of commodity OS would be very nice to have (say container isolation in a cloud environment or non-leaking of keys for a smart wallet process).

andrewchambers 10y ago
> basically, you trade a huge codebase for a smaller one in the form of the spec Most formally verified things i have seen require huge amounts of 'spec' code compared to the implementation.
- microcolonel 10y ago
  You're confusing the specification with the equivalence proof. A spec is likely going to be about as simple as an implementation, with the benefit that it can be read more consistently.
  - adrianN 10y ago
    All the specs for real world things I've seen are long and use fuzzy language. Making them formal enough to provide a basis for verification will only make them longer.

tracker1 10y ago

I think the biggest issue is from a business people perspective, formal requirements needed for this type of development (software development as an engineering discipline) is too slow, and not as open to change as the agile (craft) methods tend to be in software.

saretired 10y ago
It depends what business you're in and what your needs are. Agile doesn't get much traction in flight control software or telephone switches.
- tracker1 10y ago
  Exactly... anything dealing with critical hardware will/should be done as an engineering discipline wrt development, where tfa's practices could be better. That isn't the majority of software development, which is one-off line of business apps.

heimatau 10y ago

To save others time. I've copied some of the biggest points of the article. My comments are in [brackets], except these^^ first few sentences. "Between the lines it takes to write both the specification and the extra annotations needed to help the programming software reason about the code, a program that includes its formal verification information can be five times as long as a traditional program that was written to achieve the same end." "Jeannette Wing, corporate vice president at Microsoft Research. “Any natural language is inherently ambiguous. In a formal specification you’re writing down a precise specification based on mathematics to explain what it is you want the program to do.”" "“We’re not claiming we’re going to prove an entire system is correct, 100 percent reliable in every bit, down to the circuit level,” Wing said. “That’s ridiculous to make those claims. We are much more clear about what we can and cannot do.”" [In the experiment the article is mostly based on] "The hackers were mathematically guaranteed to get stuck. “They proved in a machine-checked way that the Red Team would not be able to break out of the partition, so it’s not surprising” that they couldn’t, Fisher said. “It’s consistent with the theorem, but it’s good to check.”" "In a return to the spirit that animated early verification efforts in the 1970s, the DeepSpec collaboration led by Appel (who also worked on HACMS) is attempting to build a fully verified end-to-end system like a web server. If successful, the effort, which is funded by a $10 million grant from the National Science Foundation, would stitch together many of the smaller-scale verification successes of the last decade. Researchers have built a number of provably secure components, such as the core, or kernel, of an operating system. “What hadn’t been done, and is the challenge DeepSpec is focusing on, is how to connect those components together at specification interfaces,” Appel said."

mkstowegnv 10y ago
"Jeannette Wing, corporate vice president at Microsoft Research. “Any natural language is inherently ambiguous." Lojban (nee Loglan) is a conlang designed to be syntactically unambiguous but as usable in speech and thought as a natural language https://en.m.wikipedia.org/wiki/Lojban_grammar https://en.m.wikipedia.org/wiki/Lojban_grammar

alexchantavy 10y ago

> “We’re not claiming we’re going to prove an entire system is correct, 100 percent reliable in every bit, down to the circuit level,” Wing said. “That’s ridiculous to make those claims. We are much more clear about what we can and cannot do.” This is an important statement that should be highlighted more prominently in the article (whose title I disagree with). Formal methods are promising, and I'm glad that the researcher acknowledged that when your project relies on so many other abstractions and systems it doesn't matter how rigorously developed your solution is if a hacker can find a way to accomplish their objective through one of your dependencies.

rocqua 10y ago
Specifically, hardware level exploits are wholly disregarded by formal verification. This means bit-banging could still work. In many systems I'd also be wary of the OS itself.
- nickpsecurity 10y ago
  They're disregarded by software verification. There's more formal verification deployed in hardware than software. There's also techniques to verify hardware and software together. The hardware problems you see are often deliberately left in there either due to corner cutting or backward compatibility with bad designs of the past. Both inspired by desire to see the number next to net income continue to rise. ;)

eriknstr 10y ago

I Google'd HACMS project and found an Open Catalog page at DARPA with a bunch of links to open source software and paper PDFs. Seem worth checking out to anyone whose interest was piqued by the article. http://opencatalog.darpa.mil/HACMS.html http://opencatalog.darpa.mil/HACMS.html

kelvin0 10y ago

A while back I was exploring the use of 'soft' formal methods to help in evaluating correctness of some new modules we had to develop. I had come upon Alloy, which seems like a gentler introduction to formal methods (Unlike Z or Coq). http://alloy.mit.edu/alloy/ http://alloy.mit.edu/alloy/ Anyone have any experience using Alloy, or some other formal method?

maramono 10y ago
I've used it several times but the big problem with it is that once you have a nice, correct model that has been checked (and no counterexamples found), there's no way to translate it to code. This meand that your basically back on square one in terms of implementation. I really like (and use quite often) the ASM method instead. More of my thoughts here: http://ortask.com/how-i-designed-built-and-tested-a-temperature-logger-with-arduino-part-2/ http://ortask.com/how-i-designed-built-and-tested-a-temperat...
- nickpsecurity 10y ago
  There's actually been imperative extensions and prolog compilers for it. Here you go: https://homes.cs.washington.edu/~emina/pubs/alloy.mscs13.pdf https://homes.cs.washington.edu/~emina/pubs/alloy.mscs13.pdf Also, for ASM's, the most interesting one I've seen is certified compiler project that is taking a lot less lines of code than CompCert: https://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf https://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf

phantom_oracle 10y ago

Here are my questions (to anybody with knowledge of this field): - Is this type of programming related to the functional-programming field? - How is this different to OOP/imperative code? - What language(s) will be used to write code for this?

AstralStorm 10y ago
I can speak about Isabelle/HOL specifically only. 1) functional programming is a subset of mathematical proofs. Isabelle syntax is somewhat similar to what is offered in ML family of functional languages. Unlike functional languages, you can use more advanced constructs than bijections (can model superposition etc.) and it is easier to state things over sets. 2) imperative code is a subset to this too with added order of operations. Language is somewhat different though Isabelle has a module that has necessary proofs to verify imperative programs.

acfoltzer 10y ago

I'm one of the researchers at Galois who's working on the quadcopter platform for HACMS. Let me first say that this headline makes me cringe just as much as anyone. I'd also like to give folks a pointer to some of the work we've developed on the project–it's all open source. First we have Ivory, the DSL for doing safe systems programming that takes buffer overflows and other memory-safety bugs off the table: http://ivorylang.org/ http://ivorylang.org/ [1] Second, the flight control software we wrote for the 3DR Iris+: http://smaccmpilot.org/ http://smaccmpilot.org/ The adventurous among you who fly with a Pixhawk can build it and try it out yourselves, and we'd love to hear your thoughts. [1]: When we began work on HACMS, Rust was around but nowhere near mature enough to base a proposal on. These days, it covers a lot of the same bases, although currently Ivory is more suited for formal analysis with SMT solvers and model checkers.

eggy 10y ago
Glad to hear you say that. Aside from that the work seems very interesting. I am going to check out Ivory. I have been reading up and playing with Idris and F. I like F so far, and that you can output F# and OCaml. Idris's goals seem in line with what you were originally looking for. Have you evaluated it?
- eggy 10y ago
  [Edit] Replying to my post to edit, since no choice given to edit. Should say "I like Fstar" above, but asterisk turned on italics...
- acfoltzer 10y ago
  Indeed, we're fans of Idris here, and even hosted a series of Idris tech talks: https://galois.com/blog/2015/01/tech-talk-dependently-typed-functional-programming-idris-1-3/ https://galois.com/blog/2015/01/tech-talk-dependently-typed-... The goals of Idris and similar languages are different from the goals we had with Ivory, though. We sometimes describe Ivory as "medium-assurance" as opposed to the high assurance one can get from a language with a more expressive type system. It makes sense for some systems or components to be formally verified, for example the seL4 verified microkernel which is also used on our copter. However we simply would not have been able to formally verify (or even get to typecheck with fancier dependent types) something on the scale of an autopilot given the resources we had on the project. Instead we rely on getting quite a bit of bang for the buck with the memory safety features, and then augment with assertions. We ended up with a working autopilot (and board-support package with drivers) in only ~4 engineer-years, so we think the tradeoff is working well so far :)

mirceal 10y ago

For anybody interested in this field: Specifying Systems by Leslie Lamport, the same guy that gave us Logical Clocks and Paxos (free on Ms Reseach website): http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/bo...

neilellis 10y ago

This article was just wildly misleading, the title is well, it speaks for itself. Interesting language and rather than 'formally proven' as the article wildly claims it is a strongly typed system ala Haskell. So yep looks a great idea for secure systems - but formally proven - bah! :-) Has anyone here actually formally proved a non trivial program, say a couple of hundred lines on NCSS? How about tens of thousands, hundreds of thousands or millions of lines of code. The complexity of the proof would be insanely complicated such that the level of expertise to define the requirements would be (if at all within the limits of human endeavour) only for maybe a handful of people. And do those people make good business analysts, or hackers, or entrepreneurs or even just communicators. Jeez the misinformation that gets spread!

tzs 10y ago
> Has anyone here actually formally proved a non trivial program, say a couple of hundred lines on NCSS? I don't know what NCSS is, so am going to answer as if your sentence stopped two words earlier. How about the CompCert C compiler [1]? Or CakeML [2]? And let's not forget seL4 [3], which has a formal proof that the implementation in C conforms to the specification, and a further formal proof that the binary code is a correct translation of the C code. [1] http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html [2] https://cakeml.org https://cakeml.org [3] https://sel4.systems https://sel4.systems

bikamonki 10y ago

Just thinking out loud: if a program can check the correctness of another program against a formal spec, can't it just write the checked program from the spec?

dougws 10y ago
You've just invented the field of program synthesis, which is a super active research area right now in programming languages! Here's the paper list from a class at UW focused on this area: http://courses.cs.washington.edu/courses/cse599a2/15wi/ http://courses.cs.washington.edu/courses/cse599a2/15wi/ . The Sumit Gulwani paper from the first week is a really good introduction to the field.
derkha 10y ago
Aside from program synthesis, there is the more restricted form of code extraction, which turns definitions inside a theorem prover into code in a more traditional, runnable language such as OCaml. But you'll still want to do one or more refinement steps inside the theorem prover where you turn your spec into more efficient definitions (or even definitions that are computable at all - how do you evaluate an unbounded universal quantifier?)
stale2002 10y ago
Well then the spec isn't just a spec. It is a programming language in and of itself. And how do you prove that THAT spec is correct? It is turtle specs all the way down.
- Crespyl 10y ago
  Sooner or later your spec language is just English and you have to get the lawyers involved. ;)
usgroup 10y ago
Have a look at Why3 for example or Coq. That's exactly what formal verification systems do: 1. Formally prove intention. 2. Generate code.
10y ago

walter_bishop 10y ago

Such 'hacker-proof code' can only be as secure as the underlying hardware. If such a cure already existed, we wouldn't be subjected to the current hacking/phishing epidemic. "these malfunctions could be as simple as a buffer overflow" No amount of 'formal verification' will detect or prevent buffer overflows, which are a defect in how the hardware allocates memory. The cure must also be found in the hardware. "Back in the 20th century, if a program had a bug, that was bad, the program might crash, so be it,” It must of been on a different planet, cause I can remember using networked computers in college way back in 1984. and the first Internet worm occurred in 1988.

marcoperaza 10y ago
Hardware bugs are NOT the major source of widely-exploited vulnerabilities in practice. They're a tiny fraction of exploits being used in the wild, and certainly of the ones being used to target the general population. Further, a buffer overflow is absolutely not a defect in how hardware allocates memory. It's a logical flaw in the software that reads/writes beyond the limits of the memory the programmer intended to access.
- mistaken 10y ago
  It's also worth noting that some critical hardware components (e.g. CPUs since the infamous division bug) are formally verified as well, so manufacturing defects should be the largest concern for them.
  - AstralStorm 10y ago
    Only a tiny fraction of the CPU is formally verified. There are frequent errata. And plenty of undefined behaviour as well as races you can hit if you really try.

peterbonney 10y ago

Aside from the obvious point that software can obly be as secure as the hardware it runs on, isn't Gödel's incompleteness theorem a problem with scaling from smallish problems to biggish ones? Granted it has been a long time since I understood it even moderately well, but my main recollection is that a complete system of logic can't be consistent, and a consistent system can't be complete. That would seem to be an issue with extending formal methods to any computer system of broad general use. Or am I misapplying the theorem here?

Jweb_Guru 10y ago
Static type systems were explicitly designed to get around various inconsistency problems with standard formulations of mathematics (ZFC, etc.). Formal verification generally exploits such type systems. In a nutshell, the incompleteness theorem (and related problems) only apply to sufficiently powerful logical systems (namely, those that can model Robinson arithmetic). Less powerful (or, in some cases, incomparable) axiom schemes exist that are capable of being both consistent and complete. Usually, the cost is that (1) they are not capable of expressing all programs (but many people argue that they are capable of expressing all useful programs), and (2) some programs that are correct in those type systems may require exponentially larger proofs (types) than a less stringent system would require in order to accept the same term (again, many people argue that this does not matter in practice).
- peterbonney 10y ago
  Also interesting - thank you.
MrManatee 10y ago
Gödel's incompleteness theorems are more of a theoretical limitation than a practical one. Roughly speaking, Gödel's incompleteness theorems say that all proof systems for number theory are limited in some way. For example, first-order Peano arithmetic is such a system, and one of its limitations is that it doesn't support transfinite induction. (It doesn't matter if you don't know what it is.) In other words, if you want to translate a mathematical proof to Peano arithmetic, you have to come up with a way to do it without transfinite induction. Sometimes, such in the case of Goodstein's theorem, this is impossible. To prove Goodstein's theorem, you have to choose a stronger proof system to begin with. So, Gödel's theorems guarantee that no matter how strong you proof system is, there are always number-theoretic statements that are beyond its reach. But for reasons that are not currently completely understood, this doesn't really happen in practice. "Naturally occurring" examples of number-theoretic statements almost always turn out to be provable in surprisingly weak systems. Instead, you run into practical problems: the theorem is provable in the system, but actually writing out the proof is utterly inconvenient. As an analogy, there are Turing-complete programming languages that don't have the concept of functions. In theory, they are capable of all kinds of computations, but in practice you don't want to use them. And if, instead of mathematics, we concentrate on proofs of correctness, then this is even less of a practical problem. To quote Leslie Lamport, proofs of correctness "are seldom deep, but usually have considerable detail." The proofs may be long and complicated, but as long as they don't use any kind of ridiculously abstract techniques, they are just the kind of proofs where computers can have an advantage over humans.

jopaki 10y ago

This is the right topic people. This is what needs to get into mainstream narratives of malware/vulns.

gravypod 10y ago

I don't get the idea of a formal method. You're attempting to prevent bugs in code by writing code that describes the final product. In any reasonably complex system the descriptions will be large, complex, and bug prone. How is a "formal method" any better then one of the following: - Unit testing: Provide every test case possible - Pure Functions: Use small methods that cannot error and always return sane values - Fuzzing Testing: To find if the implementation is actually correct or if it is correct by chance What is the benefit of a formal method? It's just inconceivable for me to see "Hacker-Proof code" and not laugh at whoever wrote this.

SolarNet 10y ago
Formal verification is a bit like using a super high level strict/static/safe programming language (often in conjunction with a classic programming language providing the actual run-time description which is being formally checked). Think C# attributes or python decorators but where they take up 80% of the code and are a language onto themselves. It basically does all of the things you described in your list through automatic formal mathematical proofs, rather than relying on chance or on the programmer directly (obviously if you write a backdoor into a formal requirement it'll make it past the proving step). - No need to unit test specific cases when all the cases have been formally proven. - Formal proving methods typically work best (or at least most easily) on pure functions for the reasons you described. - No need to fuzz random values when the entire range has been formally proven. If you ever took a theoretical computer science where the teacher had you write the formal induction proof for a loop, it's like that, where every possible case must be covered mathematically. We've simply gotten the computer to deduce the proofs for us automatically. For example if there is a global integer that can be between 0 and 700, or the value 1000, then the formal verification system will make sure nothing in the program can write any other value to that memory. It will never increment or decrement when a 1000 is in there, it will never subtract 20 when a value less than 20 is in there, etc. Including by buffer overflows, or by pointer arithmetic in some random function, or by a runaway parsing algorithm. And then we do that for ever piece of memory, every subroutine call, and every possible input. And then we prove we covered every case and never violated our spec. And we can add implications to our spec. For example the only way a command to launch a missile can happen is if the launch missile function is called, no other function no matter the state of the program can cause it to happen. This can prove that there aren't exploits to a complex program that might cause unwanted behavior. Can you prove that sort of thing to me about your software? Like can you prove to me your software is unbreakable? This solution can (with a much smaller error rate than "well I tried 17 things and none of them worked." because it can say "I tried literally every possible thing."). It's a proactive solution. We are proving that it's mathematically impossible to break (engineering still being the weak point). That's an order of magnitude, if not more, better than what we have now.

TwoBit 10y ago

All we need now is a proof that the proof program is correct. And a proof that the proof proving program is correct.

pka 10y ago
Exactly :) And a proof that the spec is correct. But without formal verification both your spec and the implementation may be incorrect.
AstralStorm 10y ago
Internal consistency is relatively easy to verify. Completeness to some extent as well. The manual task is to verify all the assumptions.

Mao_Zedang 10y ago

I have always been interested in this area of programming. One thing I have always wanted is the ability to enforce restrictions on data types beyond memory. By that I mean say i am using an int, what if I want to restrict this to actually 1 -55 you can solve this using run time error handling but wouldnt it be better if we had static checks where upstream we could see an unbounded int being passed into this method and throw a compile error.

manmal 10y ago
I think you could do that, but as long as you allow the usual operations on bounded variables (say, multiplication), you would have to ensure that the other operand is also bounded, or else you get an unbounded result nonetheless. Meaning, all variables that are used in any expression would have to be bounded eventually. There's also the problem that the compiler would have to infer that [1-10] - [1-2] can be negative, but does not have to. So with every expression on bounded variables, you increase their bounds' range, likely deleting the system's benefits.
- Mao_Zedang 10y ago
  I agree its super complex, these bounds wouldn't be limited to integer based variables. I would also argue there are very narrow instances where you would want to bound a variable and also do arithmetic on it. The language should make the bounding optional and unbounded possible.
tome 10y ago
Check the liquid type of digitsP here: http://conscientiousprogrammer.com/blog/2015/12/23/24-days-of-hackage-2015-day-23-liquid-haskell-refinement-types-for-the-real-world/ http://conscientiousprogrammer.com/blog/2015/12/23/24-days-o...

eggy 10y ago

This is a big win for Haskell, since government contracts and approved vendors tend to have long arcs of doing future business. The idea an EDSL in Haskell was used greases the skids for any future Haskell acceptance on jobs. Good luck!

TickleSteve 10y ago

Although good, hasn't this just shifted the burden up a level? With formal methods, we can get proven-ish correct implementation, now we need bug-free specifications.... this in itself will be the next challenge. In the real world, specifications are very incomplete and fuzzy, partly because the business-level specifications are also fuzzy. This will not be a panacea, its simply shifted the burden up to a (possibly more manageable) level.

nickpsecurity 10y ago
"With formal methods, we can get proven-ish correct implementation, now we need bug-free specifications.... this in itself will be the next challenge." That's much better. See, before you needed to (a) understand a vague specification, (b) get your concrete version of it right, and (c) implement that specification. Now, you just trust a precise specification. That it's precise, esp if in Z or something, let's you check it against the people giving you vague stuff too by asking them questions. Solves lots of problems. Altran/Praxis Correct-by-Construction provides an illustration of how that works: http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf At another extreme, some companies capture requirements in formal logic then just compile them to code with logic programming languages like Mercury: http://www.missioncriticalit.com/development.html http://www.missioncriticalit.com/development.html Note: Not sure how well the last one works but worth mentioning that it's at least possible to go from specs to code in some places.

usgroup 10y ago

You might regard unit tests and formal proof to be opposite ends of the same scale with model driven testing being somewhere in between. One may be well advised to pick according to what you need. Formally proving the behaviour of your whole web app would likely take you an order of magnitude longer to write.

jbb555 10y ago

I don't understand this. In order to use formal verification you have to provide a complete and correct specification of what you want the software to do. We already have formal languages for doing this called programming languages. How is this any different from a programming language?

danpalmer 10y ago
Programming languages range in their formality. At the low end you have things like Python or Ruby, where you can write a loop over a type that can't be iterated, and it will crash at that line of code. In the middle you have languages like Java, C#, at the mid-high end, even Haskell and F#. In these languages they enforce type safety at varying levels throughout the code, by first inferring the types at each point throughout the code, and then seeing whether they are consistent. You would not be able to loop over a non-iterable object here. At the really high end you get into the realm of languages like Idris, Agda, and Ivory, and "formal verification" techniques. At this level you can not just write a loop, but you can write a loop that it is possible to prove terminates regardless of the input to the loop. This is done by setting constraints, and proving those constraints all the way through the code - the compiler will infer a lot of this, but it is still more work. This is a very simplified view of it, but essentially the more formal you get in the specification, the less chance that the program can do something unintentional, crash, or be hacked. The vast majority of the code written today is not that formally specified.
fmap 10y ago
Programming languages have to be (efficiently) executable, specifications can be logical/declarative. E.g. in a specification I can state things like "forall functions, with uncomputable property foo, we have bar". Plenty of things are uncomputable (e.g. quantifiers over natural numbers), but useful in specifications. There are good and bad specifications, same as for programs. For the semantics of a programming language you could essentially transcribe an interpreter in the form of a structural operational semantics and these are relatively error prone. Instead, you could give an axiomatic semantics, which is a lot more high-level. An equivalence proof between the two gives you a high level of assurance that the operational interpretation you had in mind while writing your interpreter actually means what you think it means. A recent example, the formal specification of the weak memory model of C11 turned out to be wrong (in the sense that it forbids common compiler optimizations, because programs have access to a time machine), but this was discovered when trying to develop a program logic for C11. In practice, most broken specifications I have seen were written by people who never really worked in formal verification. I am not aware of a single instance where a piece of formally verified code was broken because of a broken specification. There are cases where the specification had to be extended. E.g. CompCert was initially developed as a whole program compiler and the spec had to be extended for separate compilation. This broke the alias analysis.

virgulino 10y ago

"Beware of bugs in the above code; I have only proved it correct, not tried it." (Donald Knuth)

AstralStorm 10y ago
Statement hopefully obviated by seL4 Isabelle to/from C compiler.

lordnacho 10y ago

Can we get an actual example of a formally verified piece of code? If I have a function adding a and b, how does it look when it's "formally verified"?

nickpsecurity 10y ago
Good news is that most of them abstract the stuff away for common operations. They'll let you annotate code that's transformed into a set of verification conditions that the prover automatically discharges. SPARK is an example: http://www.skein-hash.info/SPARKSkein-release http://www.skein-hash.info/SPARKSkein-release Let's say that work isn't done. Then you have to hand model the properties of what you're doing. Arithmetic, expressed in bits, is harder than it appears to describe in a way that covers all the properties. Here's one on SmartMIPS: https://staff.aist.go.jp/reynald.affeldt/documents/affeldt-jssst2006-en.pdf https://staff.aist.go.jp/reynald.affeldt/documents/affeldt-j...