[HN Gopher] Verified Rust for low-level systems code
___________________________________________________________________
Verified Rust for low-level systems code
Author : gz09
Score : 60 points
Date : 2024-05-04 17:50 UTC (5 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| jimsimmons wrote:
| What exactly do SMT systems "solve" in cases like this?
|
| If I wrote a simple BFS or DFS and enumerated the search space
| how far would I get.. Is that not what TLA+ does in principle.
|
| I am surprised people prefer having a dependency of something
| like Z3 at compiler level.
| IshKebab wrote:
| They try to find a counter-example to the constraints you have
| set up, or tell you that no such counter-example exists, in
| which case your program is correct. The counter-example is in
| the form of inputs to your program or function.
|
| It looks like the TLA+ Proof System does the same thing, but I
| believe you can also use TLA+ in "brute force all the states"
| mode. I haven't actually used it.
| IshKebab wrote:
| Interesting! Looks most similar to Creusot. The syntax is
| definitely nicer but wrapping your entire code in a macro surely
| is going to upset rust-analyzer?
| tsujamin wrote:
| I'm not sure how rust-analyser works, but presumably you'd make
| the macro a no-op and just return the original tokens in debug
| builds
| jaybosamiya wrote:
| A fork of rust-analyzer, called verus-analyzer, provides
| support for Verus syntax and actions (including new proof-
| specific actions) https://github.com/verus-lang/verus-analyzer/
| sdsd wrote:
| Noob question from someone with little real CS experience, when
| the README for this project says:
|
| > verifying the correctness of code
|
| What is the difference between "verifying" the correctness of
| code, as they say here, vs "proving" the correctness of code, as
| I sometimes see said elsewhere?
|
| Also, is there a good learning resource on "proving" things about
| code for working programmers without a strong CS / math
| background?
|
| Edit: I'm also very curious why "zero knowledge" proofs are so
| significant, and why this is so relevant. Eg I heard people
| talking about this and don't really understand why it's so cool:
| x.com/ZorpZK
| dumbo-octopus wrote:
| Verifying and proving are used synonymously, as made clear
| later in the opening paragraph.
|
| As for zero knowledge proofs, there is little practical use,
| significance, or relevance to them due to the overhead involved
| and the lack of a "killer app", so to speak. But they're
| conceptually interesting.
| vlovich123 wrote:
| Whenever I hear people talk about the lack of practicality of
| some mathematical construct, I always remember G H Hardy who
| worked on number theory at the turn of the century. One of
| his famous quotes I love is:
|
| > I have never done anything 'useful.' No discovery of mine
| has made, or is likely to make, directly or indirectly, for
| good or ill, the least difference to the amenity of the
| world.
|
| Despite his self-proclaimed focus on pure mathematics,
| Hardy's work, particularly in number theory, has had profound
| applications in cryptography and other fields.
|
| I agree about the overhead. The costs have come down
| significantly already but they still remain a few orders of
| magnitude too large. That being said, it's killer app is
| cloud compute. Right now the only way to amortize the cost of
| HW is to run it on someone else's computer, which brings
| along with it all sorts of security and privacy risks. Well-
| performing ZK proofs (which we don't know if it exists / it
| may be a long time before we figure out how to do it) would
| let you do cloud computing securely without worrying about
| vulnerabilities in your cloud provider's network. Like all
| cryptography, it's a double-edged sword because the same
| techniques would let websites deliver code for your machine
| to execute that you have no knowledge of what it's doing.
| IshKebab wrote:
| > What is the difference between "verifying" the correctness of
| code, as they say here, vs "proving" the correctness of code,
| as I sometimes see said elsewhere?
|
| In this context it is the same.
|
| > Also, is there a good learning resource on "proving" things
| about code for working programmers without a strong CS / math
| background?
|
| I wish. The Dafny docs are pretty good but IMO formal software
| verification is not really at the point where it is usable for
| normal programmers like us who don't have a PhD in CS / maths.
| The examples make it look relatively easy, but you will quickly
| run into "nope, couldn't prove it" and the answer as to why is
| some hardcore implementation detail that only the authors would
| know.
| dumbo-octopus wrote:
| Formal software verification encompasses a wide set of what
| we refer to as advanced mathematics. The process of taking
| some thing you want the code to do, correctly abstracting it
| out into component lemmas, and generating proofs for those
| lemmas, is itself advanced mathematics. I don't really see a
| way that this could be simplified.
| LoganDark wrote:
| AFAIK, zero-knowledge proofs allow you to prove that you know
| something without revealing what it is you know. For example,
| verifying you know a password, but without having to send the
| password to the server, so a malicious server or MitM wouldn't
| be able to sniff it.
|
| It also might provide better options for identity verification,
| i.e. proving you have a certain government-issued ID but
| without actually leaking the document to the server (for it to
| be stored "for a maximum of 2 years / 3 years / 6 months /
| etc." but then leaked in a data breach anyway).
| dumbo-octopus wrote:
| Secure password verification does not require anything close
| to what we mean when we refer to modern "zero knowledge
| proofs". A better example would be verifying you know the
| answer to a SAT problem without sharing the answer. Which is
| of... limited.. practical application.
| LoganDark wrote:
| I never said it required ZKP.
| dumbo-octopus wrote:
| You implied it would be a helpful tool for soling that
| particular problem, which is to dramatically misrepresent
| their utility to the parent asking for concrete examples
| of their relevance.
| vlovich123 wrote:
| ZK proofs could be used to implement secure cloud computing
| where a total compromise of a vendor's machines / network
| wouldn't in any way compromise the customers running
| workloads on that network.
| wk_end wrote:
| > Also, is there a good learning resource on "proving" things
| about code for working programmers without a strong CS / math
| background?
|
| I don't know how difficult Software Foundations is for someone
| with a limited background but it's probably worth trying:
|
| https://softwarefoundations.cis.upenn.edu/
| opnitro wrote:
| A very good resource for both verifying code and functional
| programming is Software Foundations
| (https://softwarefoundations.cis.upenn.edu).
|
| One note though: Verus and the tool Software Foundations works
| with (Coq) take different approaches to proving things.
|
| Verus attempts to prove properties automatically using
| something called an SMT solver, which is an automated system
| for solving constraints. Coq on the other hand, requires you to
| manually prove much more, offering a more limited set of
| automations for proving things.
|
| Both have their advantages and disadvantages, namely that
| automation is great when it works and annoying when it doesn't.
|
| (Another side note: Zero Knowledge Proofs (ZKPs) are kind of
| something different. A great many people who work in formal
| verification/proof don't touch ZKPs at all (ex: me). They are
| better thought about as a cryptography primitive)
| binary132 wrote:
| Verification is proving specific things about specific
| properties of the program.
| dist1ll wrote:
| One of the main contributors gave an excellent talk [0] on Verus
| at the Rust meetup in Zurich. I was really impressed how clean
| this "ghost" code fits into programs (reminded me a bit of Ada).
|
| [0] https://www.youtube.com/watch?v=ZZTk-zS4ZCY
| TachyonicBytes wrote:
| Is there any relationship between this and Kani[1]? Do they work
| differently?
|
| [1] https://github.com/model-checking/kani
| mmoskal wrote:
| Model checkers typically only explore a bounded number of
| states which is efficient at bug finding and often doesn't
| require additional annotations in the program.
|
| Automatic (SMT-based) verifiers like Verus, Dafny, F* (and my
| VCC :) require you to annotate most every function and loop but
| give you broad guarantees about the correctness of the program.
|
| Tools based on interactive provers (like Coq or Lean) typically
| require more guidance from the user but can guarantee even more
| complex properties.
| im3w1l wrote:
| This looks really cool. One thing I think would be really useful
| for people is some instructions / examples of how to add proofs
| for an existing codebase.
|
| So maybe an example could be a bare-bones gui app with a single
| textbox, that does an http request to some resource (having data
| that is unknown at compile-time and potentially untrusted is a
| very common thing) and fetches an array, which is bubble-sorted
| and displayed in the box. The bubble sort has some intentional
| bug (maybe due to some off by one error, the last element remains
| untouched). There are unit-tests that somehow don't trigger the
| bug (worrying that your tests are incomplete would be a primary
| motivator to go for proofs). It could then show how to replace
| the unit tests with a proof, in the process discovering the bug
| and fixing it.
|
| The example wouldn't need to go into huge detail about the proof
| code itself as it is potentially advanced, instead it would focus
| on the nitty-gritty details of adding the proof, like how the
| interface between proved mathematical code and non-proved io code
| works, what command line to run to prove&build, and finally a zip
| archive with all of that, that you can play around with.
___________________________________________________________________
(page generated 2024-05-04 23:00 UTC)