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

71–80 of 96 posts

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

#71

Post by pron »

nickpsecurity wrote: post #43
pron wrote: post #28

Earlier quoted context omitted.

No need to use Ada, though. Similarly powerful options exist for Java and C. The code-level specification language is JML (Java) or ACSL (C), and there are many verification tools, from SMT solvers, through proof assistant obligations, to concolic or randomized test generation. Nevertheless, you're never certain doing that, either, as you don't formally tie the code-level specification to the high-level specification…

They exist but SPARK's were much better on automated proving. It was due to SPARK being a simpler language designed explicitly for verification.

Right, but this is because SPARK is (intentionally) limited. For example, AFAIK, you can't dynamically allocate memory in SPARK. If you write Java code that is as simple as SPARK code, it would also be automatically verified (after all, the solvers are the same). Java also has automated verification that does separation logic, and works well with dynamic memory (Facebook's Infer).

Languages that truly admit full automatic verification (and are also limited) -- including rich global correctness properties -- are synchronous languages for safety-critical realtime, like SCADE. BTW, SPARK contracts are not so rich. There are many useful properties that you can't express.

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

#73

Post by hoodunit »

eridius wrote: post #67
EGreg wrote: post #66

Earlier quoted context omitted.

Whenever you put a comment, chances are you should have encapsulated the block there into a reusable block of code.

Why? 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.

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

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

#74

Post by samth »

nickpsecurity wrote: post #65
samth wrote: post #64

Earlier quoted context omitted.

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

I think the one you're talking about got the TCB down to a few hundred lines of C. Done in Twelf.

No, I'm talking about the one I linked to, which is done in Coq.

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

#75

Post by samth »

dronemallone wrote: post #31
munin wrote: post #11

Earlier quoted context omitted.

This 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…

That "facility" is the Curry-Howard correspondence!

Extraction 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.]

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

#76

Post by nickpsecurity »

kibwen wrote: post #70
nickpsecurity wrote: post #68

Earlier quoted context omitted.

Which Frama-C, Simpl/C, and Astree Analyzer all do. Then that C code is quite trustworthy. Rust has stuff like Simpl in the works but needs something like Frama-C or SPARK for unsafe.

Can you give me an example of something that safe Rust doesn't allow, thereby requiring the unsafe keyword to implement, but that also contains an error that passes the Rust compiler silently but that Frama-C or SPARK would statically detect?

That's a trick question: you know I don't know know Rust enough to answer it. :P However, I fo know the things I mentioned can prove safety properties about unsafe code. Rust compiler can't per these threads. So, If A then B...?

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

#77

Post by nickpsecurity »

samth wrote: post #74
nickpsecurity wrote: post #65

Earlier quoted context omitted.

I think the one you're talking about got the TCB down to a few hundred lines of C. Done in Twelf.

No, I'm talking about the one I linked to, which is done in Coq.

Oh 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

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.

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

#78

Post by nickpsecurity »

pron wrote: post #71
nickpsecurity wrote: post #43

Earlier quoted context omitted.

They exist but SPARK's were much better on automated proving. It was due to SPARK being a simpler language designed explicitly for verification.

Right, but this is because SPARK is (intentionally) limited. For example, AFAIK, you can't dynamically allocate memory in SPARK. If you write Java code that is as simple as SPARK code, it would also be automatically verified (after all, the solvers are the same). Java also has automated verification that does separation logic, and works well with dynamic memory (Facebook's Infer). Languages that truly admit full auto…

"If you write Java code that is as simple as SPARK code, it would also be automatically verified (after all, the solvers are the same)."

Java has a different model than SPARK. Especially if you're considering verifying it against the JVM or against assembly. SPARK will probably have an advantage given the papers I've read on JML work. Far as it's overall tooling, I'm aware it has a bunch for proofs and testing as it's one of three I mention to look for in supposedly, high-assurance projects (others being C subsets & Ada/SPARK). Infer is new to me, though, so thanks for mentioning it.

"BTW, SPARK contracts are not so rich. There are many useful properties that you can't express."

Hence, work like E-SPARK that combines Event-B and SPARK. Another I saw uses SPARK, TLA+, and UPAAL for timing analysis on stuff already analyzed at component level. Best to mix and match. DeepSpec with CertiKOS is probably state of the art in that far as popular stuff goes. My Brute Force Assurance concept will do it differently if I implement it where I mix automated analysis and testing tools for code generated in C, Java, and SPARK where each's toolchain catches something the others miss. Semantic mismatches could be a problem but I'm hoping something could come out of it.

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

#79

Post by nonsince »

munin wrote: post #11
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…

This 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…

If the OCaml code is Standard ML-compliant you could run it on Cake, then you only have to trust the conversion

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

#80

Post by nonsince »

seagreen wrote: post #53
roblabla wrote: post #46

Earlier quoted context omitted.

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/

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

Post reply on HN