13 ms·
Writing correct lock-free and distributed stateful systems in Rust, with TLA+
- unboxed_type 9y agoLets say you model-checked some distributed algorithm with TLA+. You then implement it in Rust. How are you going to check that your implementation implements exactly the algorithm you have checked and not some other algorithm which looks very similar? I think the phrase 'reliable systems' is more appropriate to what you are up to, as opposed to the phrase 'correct systems' which usually corresponds to formal verification.
- munin 9y agoThis is a gap in this kind of verification work. Systems like coq get around this by having a facility to "extract" code from the proof itself. You would define your algorithm as a Fixpoint, prove properties of that Fixpoint, then extract that Fixpoint into some ocaml code and use it directly in your real programs. This closes the loop you describe, insamuch as you trust the extraction process and the ocaml compiler and runtime (but other work is ongoing to close that loop as well).
- chrisseaton 9y agoThe loop is always open though. Who verifies your verification code? Who verifies the processor implementation? All you can do is reduce the gap in the loop surely?
- nickpsecurity 9y agoIt's been done down to the hardware. Originally by Computational Logic Inc for FM9001 whose prover became ACL2. Then Verisoft went from apps to OS to C subset to VAMP processor (DLX-style). Recently people are doing HOL to hardware that will integrate with HOL/Light whose core is a few hundred or thousand lines to trust. Those people eliminated trust requirements in everything from extraction mechanisms to provers to assembly generation: http://www.cse.chalmers.se/~myreen/ http://www.cse.chalmers.se/~myreen/ Follow he and his colleagues work for all that. Especially Milawa and CakeML. If you want a starting point, a small, Forth-like processor verifiable by hand on a node verifiable by eye could run the initial interpreter and prover for the first, real CPU. Plus, common practice is to split work into untrusted generation of artifacts with traces that are verified by a trusted checker that's comparatively tiny and simple. The little CPU would just run the checkers. You can run the generation on anything you like with the speed benefit. :)
- unboxed_type 9y agoWhat about real CPUs (much more complex than 'Forth CPU'), network adapters (has its own CPU), memory controllers, real OS kernels, POSIX library (which is sometimes loosely specified) and so on? As far as I understand modern truly reliable system (commerical avionics-like) still must be relatively simple to be verified up to hardware level.
- nickpsecurity 9y agoReal CPU's are formally verified for certain properties with rigorous tests. That's why they have only 100-300 errors in something with a billion transistors. That practice started after a recall. Now, for examples of full, mathematical verification of about every aspect you're looking at VAMP and AAMP7G. http://www.spbguga.ru/files/Formal_Verification_of_a_Processor.pdf http://www.spbguga.ru/files/Formal_Verification_of_a_Process... http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf VAMP is a pretty-complex, DLX-style CPU. I think they extended it to multicore or concurrency of some kind in another work. Original was single core, though. Passed all the FPGA tests. The AAMP7G combines a stack machine, over a hundred instructions, microcode engine, and separation kernel into one CPU. It was first in recent times in high-assurance security to use microcoding. I tell everyone to do that since it lets us easily change the behavior of the hardware without reverifying everything. Their tools also let you verify software semi-automatically against a model of the hardware ISA. Main stuff is paywalled but this is best free one I could get you. On availability side, they also run three units at once with a voter to reduce the odds the chip will fail. Truly high-assurance exemplar in availability and security. The prover is ACL2. You can do a trusted checker for that in few lines of code. You might need a lot of RAM and CPU time, though. Even all that can be a few blocks verified by eye and hand that you just plaster over a bunch of silicon then verify correctness automatically. There's also techniques where a partial failure can be magnified into total, visible failure. Tandem/HP NonStop does stuff like that to catch and replace failed components before system downtime happens. So, you can be reasonably sure the components are working even if defects happen during fabrication.
- deleted 9y ago[deleted]
- munin 9y agoYou can close all of those. You can have large amounts of your verifier itself be verified. You can verify the CPU design (hardware people tell me this used to be standard, and a lot of the formal methods community has roots in verifying hardware). What you can't close is the language that you use to do all the verification in, itself. You wind up with a core calculus that you have to stare at really hard and trust / prove via other means.
- DanWaterworth 9y agoYou always have to make assumptions in any formal system able to express arithmetic as proved by Gödel.
- roblabla 9y agoIsn't this susceptible to a trusting trust[0] attack, where your verifier has a bug that makes it verify itself, even though it shouldn't ? It's always possible there is a loop somewhere. The best you can hope for is make it infinitesimally small. [0]: http://wiki.c2.com/?TheKenThompsonHack http://wiki.c2.com/?TheKenThompsonHack
- mcguire 9y agoA trusting trust attack cannot be eliminated, only be made prohibitively expensive. One way to do that is by using multiple verifier back-ends.
- seagreen 9y agoThere's been a simple counter to trusting trust attacks since 2009: https://www.dwheeler.com/trusting-trust/ https://www.dwheeler.com/trusting-trust/
- nonsince 9y agoIf I understand the abstract correctly, that relies on having a trusted compiler, which assumably would have to be bootstrapped ultimately from a trusted hand-written compiler in machine code. This effectively counters malicious trusting trust attacks but does not effectively counter trusting trust attacks due to error, because your entire trusted stack has to be correct. That's not to say there's no way to close the loop here, simply that I don't know that this is it.
- samth 9y agoRight, the concept of the TCB (trusted computing base) is the important thing. Good discussions of remaining TCB in verified code are in the seL4 work, or in this paper: https://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf https://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf
- nickpsecurity 9y agoSee my link to Myreen's page and follow all those people's publications. Much of the TCB functions in papers like that has been eliminated in other work. It just needs to be cross-checked, integrated, and applied.
- samth 9y agoRight, that's one of the nice things about Appel's paper: he shows how to integrate a few different pieces to significantly reduce the TCB (ie, it doesn't include anything about C the language at all).
- nickpsecurity 9y agoI think the one you're talking about got the TCB down to a few hundred lines of C. Done in Twelf.
- samth 9y agoNo, I'm talking about the one I linked to, which is done in Coq.
- nickpsecurity 9y agoOh my bad. I just saw work such as seL4 then assumed it was a seL4 reference. I actually didn't have this one by Appel. Thanks for the paper! :) Here's the one I was referencing with the tiny TCB: https://www.cs.princeton.edu/~appel/papers/flit.pdf https://www.cs.princeton.edu/~appel/papers/flit.pdf OK. So, it was a few Kloc. Still smaller than Coq. They could probably get it even smaller with recent work given translation validation knocks compilers out of TCB. So, in between 803-2668loc.
- joshuata 9y agoAn interesting solution to this problem is verification witnesses[1]. A witness is a machine readable record of a verification task. Several different programs can read the witness and verify it independently. It is especially useful for counterexamples, where it can be a simple program trace to the error state. Given the input program and witness another can check whether the error state is reached. [1] https://www.sosy-lab.org/~dbeyer/verification-witnesses/ https://www.sosy-lab.org/~dbeyer/verification-witnesses/
- dronemallone 9y agoThat "facility" is the Curry-Howard correspondence!
- mafribe 9y agoNot necessarily. Isabelle/HOL, an prover not based on CH but on the LCF-architecture, can also do program extraction, see e.g. Program extraction in Isabelle: https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides....
- samth 9y agoExtraction of terms written using Fixpoint isn't really the Curry-Howard correspondence. Instead, the correspondence is between (for example) proofs of correctness and terms in the Calculus of Constructions. [Fixpoint terms are also CIC programs, so there's a sense in which they're related, but it's not really about Curry-Howard.]
- pron 9y agoIt's not "getting around", and one could write an extraction tool like that for TLA+, too. The difficulty is simply verifying any system, by whatever method, end-to-end, namely verifying that the high-level global correctness properties are preserved all the way down to machine code. We simply have no idea how to do it for real-world, large software, and in those cases it's been done for small, simple software (seL4, CompCert), the process was extremely expensive.
- nonsince 9y agoIf the OCaml code is Standard ML-compliant you could run it on Cake, then you only have to trust the conversion
- nickpsecurity 9y agoThat's why you implement it in Ada 2012 w/ SPARK 2014. You can encode the verification conditions as contracts. All the basic ones should be proven automatically. Those that aren't can be turned into runtime checks. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) http://www.electronicdesign.com/industrial/rust-and-spark-software-reliability-everyone http://www.electronicdesign.com/industrial/rust-and-spark-so... Here's an example of combining Event-B with SPARK to split overall verification between tools with each handling what they're good at: https://pdfs.semanticscholar.org/481c/d4d2409115429f4b824f370eb08fa338d67a.pdf https://pdfs.semanticscholar.org/481c/d4d2409115429f4b824f37...
- unboxed_type 9y agoHow well Ada/SPARK suits distributed control algorithms I wonder? As far as I understand contracts are good enough for sequential code, but not well suited for parallel/distributed computation? Runtime checks are good as to prevent something from happening, but they are not able to guarantee the absence of an error in the first place, right?
- oconnore 9y agoHuh? The whole point of distributed algorithms is that a set of local algorithms create a global behavior. I received this message so I send that message, etc. The SPARK contracts you write would check that local behavior, and the TLA+ would check that that local behavior results in some global behavior.
- unboxed_type 9y agoWell, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.
- pron 9y agoIn principle, you could translate your code -- or even the generated machine code -- back to TLA+ and check it there. This has been done as research projects for C[1] and Java bytecode[2]. But the reality of formal verification is that we simply do not yet have the capability -- with any tool -- to formally specify and verify a large, complex software system end-to-end (namely, from high-level global correctness properties and all the way down to machine code). There are two options: either use tools that can do end-to-end verification like Coq and Isabelle and limit yourself to small software, and even then expend an inordinate amount of effort (like seL4 or CompCert, small programs that have been verified end-to-end, taking years), or use any verification tool (be it Coq or TLA+) for a high-level specification and verification without extending it end-to-end, for a lowered confidence. If you like, you can augment that with code-level specification -- like JML (Java), ACSL (C), SPARK (Ada) etc.. [1]: https://link.springer.com/chapter/10.1007/978-3-319-17581-2_14 https://link.springer.com/chapter/10.1007/978-3-319-17581-2_... [2]: http://ieeexplore.ieee.org/document/6042069/ http://ieeexplore.ieee.org/document/6042069/
- nickpsecurity 9y ago"In principle, you could translate your code -- or even the generated machine code -- back to TLA+ and check it there. This has been done as research projects for C[1] and Java bytecode[2]." There's also ASM's and equational methods that allowed specification or verification of instructions or their use to happen in days when the tooling was already adequate. I wouldn't use TLA+ for this unless we're talking about concurrency. Even then, I'd be using it in combination with something else. You might also find it interesting that one group embedded TLA+ in a sound prover (HOL?) for making the TLA+ analysis sound. They extended it in some way, too. Anyway, the got the benefits of both with that combination. So, some weaknesses in the tooling can be knocked out over time if more people just put labor in.
- pron 9y agoIt all depends on your precise requirements and aesthetic preferences. I personally find TLA+ more elegant than any other high-level specification language, and very few projects actually require end-to-end verification. Those that do, must be kept small as we simply do not have the ability to do end-to-end verification of large software, no matter what tools or combination of tools we have. We don't even have a theoretical breakthrough to point us at a likely method of achieving that. If you need end-to-end verification, you must accept that the software (or component) verified will be small, and the process arduous. Then again, if you really need end-to-end verification, you must be ready to make that sacrifice. Moreover, to the best of my knowledge, no significant end-to-end verification was ever done in industry without close assistance from expert researchers, except in specialized niches where model-checkers give you sufficient coverage. Supplementing a high-level verification with code-level specification tools is always possible, but, again, everything here is a matter of the required confidence vs. affordable cost. Additional confidence always comes with additional cost.
- codemac 9y agoAs Lamport says: why do we always use blueprints before constructing a building? I agree there are some missing links, but checking your model before doing detailed implementation is a good idea regardless
- unboxed_type 9y agoAbsolutely. Anyway this gap is worth mentioning for deeper understanding of a verification problem.
- microcolonel 9y agoFor seL4, models were used to map all the way from the semantics of the instruction set to the high level model; this included a model of equivalence between the C source code and the machine code. Took them basically from 2006 to 2014 to do that (including the time to author and verify the kernel in particular).
- alexnewman 9y agoI like this a lot
- akoster 9y agoSame here!
- dikaiosune 9y agoThere's a lot of interest in formally verifying things about the unsafe subset of Rust, for example the Rust Belt project: http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/. One thing I've not well understood is how these efforts may be affected by some of the conversations around the unsafe code guidelines effort: https://github.com/rust-lang/rfcs/pull/1643 https://github.com/rust-lang/rfcs/pull/1643 https://github.com/nikomatsakis/rust-memory-model https://github.com/nikomatsakis/rust-memory-model
- vog 9y agoJust curious: Are there also attempts in the reverse direction? That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? (maybe even compiles down to the same machine code)
- ekidd 9y ago> That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? I write a fair bit of production and hobby Rust, some of it very performance-intensive. And at this point, 'unsafe' is already very rare in the code I see. The most common uses: 1. For implementing certain core data structures based on pointers. This is pretty rare—there are good implementations of just about everything I need, either from the 'std::collections' library (which uses a moderate amount of 'unsafe') or from third parties (who tend to use much less 'unsafe'). 2. For the FFI. Again, this is increasingly rare: More and more key libraries are now available as pure Rust, and the "big" C libraries typically have well-maintained bindings. 3. Theoretically, for performance. But I've written tons of high-performance, benchmarked Rust without ever touching 'unsafe'. And I do feed a fair bit of my code through fuzzers, and they've never found an exploitable weakness. So my gut feeling? There really isn't much 'unsafe' out there. And the small amount of 'unsafe' code that exists is probably—based on my experience fuzzing it—"safer" than all but the very best C/C++ code. I can live with that for now, on a strictly practical level.
- dikaiosune 9y ago
- nicknash 9y agoFor lock-free data structures, how does this verification encode the memory model? E.g. high-quality model checkers for the C++11 memory model allow for outcomes inconsistent with the execution order of the code (in addition to outcomes that aren't sequentially consistent, but are consistent with the execution order). They also work on unmodified source. In the past I've seen SPIN/Promela used as a tool for concurrency-checking, but it's silent on memory-models (implicitly sequentially consistent)
- pron 9y agoYou just define it :) TLA+ doesn't have a built-in memory model, nor any concept of memory whatsoever. You define your constructs at the level of detail you think is important. Weak memory can be defined using a CPU-local memory that is occasionally reconciled with RAM or other core-local memory.
- lenage 9y agothanks for great work
- cabaalis 9y agoRust-ignorant here; I was reading your "why rust" section. It contains a lot of information about how safe the resulting code is and how that is such a great benefit, and that's why Rust was selected. But then it has this statement: "However, it needs to be noted that when creating lock-free high-performance algorithms, we are going to need to sidestep the safety guarantees of the compiler." .... So why Rust?
- burntsushi 9y agoThe benefit of Rust is not necessarily to completely avoid unsafe (although, that does happen in practice a lot). The benefit is that unsafe can be buttoned up behind a safe API, hopefully in a way that is Zero Cost. So you might have some unsafe core that you need to pay extra special attention to, but the rest of your code can be in safe Rust. For example, I maintain a Snappy compression crate in Rust. It uses quite a bit of unsafe internally (mostly for being too clever with unaligned loads/stores), but any users of that crate never need to utter `unsafe`. If there's a bug somewhere, you can be confident it's not in the code that uses Snappy, but rather in Snappy itself, which is presumably a much smaller surface area than "all of the code."
- mhh__ 9y agoThat's still not really unique to rust, D (at least) does that too. However, good point nonetheless.
- steveklabnik 9y agoA big difference is the defaults; Rust made an explicit design decision to make unsafe the default, to mark it with a keyword and to make unsafe a superset of safe. It is totally true that these things aren't unique, but there is a lot of advantage for this specific set of choices in combination.
- staticassertion 9y ago> Rust made an explicit design decision to make unsafe the default You mean 'safe the default'.
- mcguire 9y ago"Pluscal has two forms, c and p. They are functionally identical, but c form uses braces and p form uses prolog/ruby-esque begin and end statements that can be a little easier to spot errors with, in my opinion." Nit: that should be Pascal/Ruby, no?
- EGreg 9y agoIf you're working with a language that has closures, I started to have a heuristic: // if you are writing a comment like this // explaining what the next block of code does // chances are you should just refactor it // into a closure _doWhateverCommentSaid(arg1, arg2, arg3); it's true that this needlessly adds stack overhead, but this way, you are more likely to structure your code properly, re-use it properly (which more than pays for the stack overhead), and move your closure / method to be more and more global as needed. Perhaps if you have a comment like this: f(x); // x matches some assumption then in fact, you should add validation to f itself, in the form of a function, same as above. function f(x) { _theAssumption(x); } this habit encourages re-use and proper structuring of code. in short, comments may be an anti-pattern!
- eridius 9y agoHow does wrapping up code in a closure "fix" the need for comments? And what's wrong with having comments anyway? You haven't demonstrated that comments are an "anti-pattern", all you've demonstrated is that you personally prefer a different style.
- EGreg 9y agoWhenever you put a comment, chances are you should have encapsulated the block there into a reusable block of code.
- eridius 9y agoWhy? You're saying that without any supporting evidence. And frankly, what you're suggesting sounds to me like an unreadable mess. You're going to bloat your code with closures all over the place, simply so you can attach a name to the closure, all to avoid having a simple comment. Naming closures is not a good substitute for comments.
- hoodunit 9y agoNaming closures or functions absolutely is a good substitute for a large class of comments. When you write a comment as a function name, that comment gets maintained when the code changes. It also encourages modularizing your code- often when you write a comment it's a sign that your code is trying to operate conceptually on more than one level and it would be more understandable to separate those levels. I wouldn't say comments are an antipattern but they are a code smell and should be used sparingly and only where the same explanation can't be given through function/variable naming or refactoring.
- tschottdorf 9y agohttps://github.com/uwplse/verdi https://github.com/uwplse/verdi is a good example of this (it uses coq and extractions along with minimal glue).
- unboxed_type 9y agoHave you tried it yourself or maybe you know someone who have? Honestly, I think that this development is highly impractical due to very high entrance ticket price for someone not belonging to UW PLSE group ;-)