Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Writing correct lock-free and distributed stateful systems in Rust, with TLA+

github.com

Post reply on HN
Print view View original

51–60 of 96 posts

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#51

Post by mcguire »

roblabla wrote: post #46
munin wrote: post #29

Earlier quoted context omitted.

You 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 /…

Isn'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

A trusting trust attack cannot be eliminated, only be made prohibitively expensive. One way to do that is by using multiple verifier back-ends.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#52

Post by mcguire »

dmix wrote: post #50
mcguire wrote: post #49

" 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?

> PlusCal (formerly called +CAL) is a formal specification language created by Leslie Lamport, which transpiles to TLA+ https://www.wikiwand.com/en/PlusCal

Right, but Prolog doesn't use begin/end's.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#53

Post by seagreen »

roblabla wrote: post #46
munin wrote: post #29

Earlier quoted context omitted.

You 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 /…

Isn'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

There's been a simple counter to trusting trust attacks since 2009: https://www.dwheeler.com/trusting-trust/

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#54

Post by dbaupp »

michaelmior wrote: post #9
sanxiyn wrote: post #7

Earlier quoted context omitted.

There is interest in enabling safe interface, that is, improving Rust the language so that you can provide safe interface with better performance. A good example is so-called "streaming iterator". There is less interest in changing Rust so that currently unsafe implementation (not interface) of safe interface can be made safe, that is, verified by compiler. As grandparent stated, and I agree, as long as interface is…

Maybe I'm missing something, but I could write an interface labelled sage on top of any unsafe code I want. Why doesn't it matter that my unsafe implementation is proven correct?

It would be great if it was, but it's also infeasible for a lot of code (at the moment anyway): it takes too much time and effort, and, in the FFI case, requires proving a whole external library correct too.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#55

Post by nickpsecurity »

unboxed_type wrote: post #45
oconnore wrote: post #40

Earlier quoted context omitted.

You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, and the local contract ensures that the local behavior of the various actors is correct -- and therefore results in that emergent behavior. Combined, that's a fairly solid argument that your system…

Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense. Its just a little out of scope of the current thread, because the author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.

No, I meant implementation in SPARK. The specs were already done in TLA+ in the OP's model. There's also implied porting between two notations.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#56

Post by codemac »

unboxed_type wrote: post #10

Lets 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 verific…

As 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

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#57

Post by nickpsecurity »

roblabla wrote: post #46
munin wrote: post #29

Earlier quoted context omitted.

You 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 /…

Isn'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

No. The Karger attack on compilers that Thompson talked about was mitigated far as methods to use before Thompson even published it. You just use a verified interpreter, compiler, and/or CPU for the bootstrap. Hardware is couriered with tamper-evident seals. Software built from source or at least use crypto to verify source. It's also least likely attack you'll run into: 0-days in your stuff or compilers optimising away security is more common.

A medium-assurance solution is 3+ compilers with same input and output on diverse hardware by diverse teams unlikely to collude all producing ssme result. If hardware, you can do that with chips plus voting scheme.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#58

Post by nickpsecurity »

samth wrote: post #48
chrisseaton wrote: post #12

Earlier quoted context omitted.

The 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?

Right, 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

See 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.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#59

Post by nickpsecurity »

munin wrote: post #29
chrisseaton wrote: post #12

Earlier quoted context omitted.

The 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?

You 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 /…

To support your point, Jared Davis and Magnus Myreen did the Milawa prover that builds the logic and implementation in layers starting with a hand-checked, tiny logic. Builds all the way to first-order prover with each layer getting re-checked by those below where feasible. Uses Myreen's method for verification to assembly (or machine code?). So, it's already been done.

http://www.cs.utexas.edu/users/jared/milawa/Web/

The other approach I investigated was proving the logics sound in set theory given it's well-understood, trusted, and widely deployed by mathematicians. Once the logics like FOL or HOL are verified, we just have to verify the specs and checkers (already done to in progress). Run on diverse hardware to prevent glitches there. From then on, mainly just look at logical specs since we should be good. I also found a verified compiler that uses Z specs with Prolog code... a method that might be used with Milawa for bootstrapping trust.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#60

Post by kbenson »

cabaalis wrote: post #20

Rust-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?

I think the specific portion in that paragraph you should focus on is:

We are giving up a significant benefit of Rust for certain very high-performance chunks of this system. In place of Rust's compiler, we use the TLA+ model checker to gain confidence in the correctness of our system!

With special emphasis on "very high-performance chunks of this system". There's still quire a lot to be gained by having a a lot, or even most, of the system with certain aspects of safety assured. It's not an all-or-nothing proposition, and that's a feature.

Personally I think it's very cool to then take these portions that they can't or won't use the built-in rust safety mechanisms for and do modeling to provide extra levels of assurance. It's probably also quite a boon to this process to have high assurances for much of the system as it may reduce the space (states) which you must model.

Post reply on HN