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

Re:Writing correct lock-free and distributed stateful system... by nickpsecurity on Friday May 19, 2017 @07:53AM (#14374708)

It'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/

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. :)

[ Parent | on HN ]

Re:Writing correct lock-free and distributed stateful system... by unboxed_type on Friday May 19, 2017 @08:09AM (#14374805)

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

[ Parent | on HN ]

Re:Writing correct lock-free and distributed stateful system... by nickpsecurity on Friday May 19, 2017 @09:27AM (#14375369)

Real 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_Process...

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.

[ Parent | on HN ]