6 ms·

You know, I'm not really into cryptocurrency, but it does seem like it's contributing to a resurgence of interest in formal methods. So - thank you, cryptocurre

You know, I'm not really into cryptocurrency, but it does seem like it's contributing to a resurgence of interest in formal methods. So - thank you, cryptocurrency community!

galangalalgol 5y ago
I've worked on safety critical software, but we did not use formal methods. Lots of test and checking for coverage (at asm level). Oodles of static analysis and wading through false positives. Do formal methods usually supplement those or replace some of it? Can provers or formal methodologies scale to safety critical codebases of 100s of ksloc? Whether such codebases should exist, or be better partitioned is a separate issue.
- notimrelakatos 5y ago
  Formal methods seems to be perfect for verifying protocols, specially finding design flaws, here an example of an ongoing effort to verify TLS https://www.mitls.org/ https://www.mitls.org/ https://github.com/project-everest/mitls-fstar https://github.com/project-everest/mitls-fstar
- someguyorother 5y ago
  The current crowning achievement of formal methods is, as I understand it, seL4. It is a formally proven microkernel of about 8500 LOC. There's still a while to go until they can scale to 100kLOCs, unfortunately.
  - nextaccountic 5y ago
    CompCert is also very impressive. It's not, however, free software / open source (the source is available though) https://www.absint.com/compcert/structure.htm https://www.absint.com/compcert/structure.htm A problem with both seL4 and CompCert is that the code written to express the proofs is huge, much larger than code that actually does stuff. This puts a ceiling on the size of the projects we can verify. F* is a language that tries to address that, by finding proofs with z3, a smt prover; z3 can't prove everything on its own but it cuts down proof code by orders of magnitude. They have written a verified cryptography stack and TLS stack, and want to write a whole verified http stack. https://www.fstar-lang.org/ https://www.fstar-lang.org/ https://github.com/project-everest/hacl-star https://github.com/project-everest/hacl-star https://www.mitls.org/ https://www.mitls.org/ https://project-everest.github.io/ https://project-everest.github.io/ F* (through Low, a verified low-level subset of F) can extract verified code to C, which is kind of the inverse than the seL4 proof: seL4 begins with C code and enriches it with proofs of correctness; hacl* (a verified crypto F* lib) begins with a proven correct F* code and extracts C code (I gather the actual crypto primitives is compiled directly to asm code because C has some problems with constant time stuff). This enables hacl* to make bindings to other languages that can just call C code, like this Rust binding https://github.com/franziskuskiefer/evercrypt-rust https://github.com/franziskuskiefer/evercrypt-rust Also this F* stuff is all free software / open source, so it might become a very prevalent crypto and TLS stack
- retrac 5y ago
  Not as a monolithic object. You might be able to do it with an almost microkernel approach (whatever you're implementing) with multiple small, well-defined objects with a well-defined protocol between them. That can be very useful. But I doubt you could formally verify their collective behaviour. The space and time complexity of the algorithms is explosive as the number of interacting objects increases.
  - maweki 5y ago
    Note that the specification (what you prove correctness of the implementation against) already grows with the number of interactions.
- tombert 5y ago
  I've never really worked on anything safety-critical, but I know that at least one real-time operating has been designed and verified with TLA+ [1]. The book is a bit pricey (and used copies don't pop up that often), so I haven't read it, but my understanding is that the developers felt that TLA+ did find bugs. That said, TLA+ is written separately from the code. There could of course be bugs in the translation of TLA+ -> C...TLA+ is about checking the design itself, not the code. [1] https://www.springer.com/gp/book/9781441997357 https://www.springer.com/gp/book/9781441997357
- noneeeed 5y ago
  Yes, they are normally used in conjunction with testing. But they are also used in conjunction with careful systems engineering to minimise the amount of code that needs to go through the most rigerous processes and focus on what really mattered. I'm curious which static analysis tool you were using. I used to work in SPARK Ada and false positives were not really a thing due to how it worked. But I've heard of others that were much less restrictive which ended up with lots of false positives, or "maybe" cases that then wasted everyone's time. I can see how systems like that would put people right off using them.
- diroussel 5y ago
  AWS have worked with Leslie Lamport of proving properties about S3. See: Use of Formal Methods at Amazon Web Services https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....
X6S1x6Okd1st 5y ago
Another public good that cryptocurrency has been contributing to is advances in zero knowledge proofs including some really interesting stuff like SNARKs
- tromp 5y ago
  Here's the state of the art on that: https://iacr.org/cryptodb/data/paper.php?pubkey=31249 https://iacr.org/cryptodb/data/paper.php?pubkey=31249
  - X6S1x6Okd1st 5y ago
    One thing to highlight how important this may turn out to be: > Proof-carrying data (PCD) enables a set of parties to carry out an indefinitely long distributed computation where every step along the way is accompanied by a proof of correctness. It generalizes incrementally verifiable computation This has the potential to remove the element of trust that you currently must place in the provider of computation resources. With SNARKs you can simply ask them to include a proof that they actually performed the computation that is sublinear in the length of the proof and sublinear in the amount of time taken to verify the proof. Of course this will always be more computationally expensive for the provider of the computation resources to both do the work and provide the proof.
- miketery 5y ago
  Any good tutorials? I’m having a hard time understanding some of the write ups I’ve found so far.
yjftsjthsd-h 5y ago
It also seems associated with advances in wider adoption and some progression in state of the art of functional package managers and reproducible builds, which has been nice to see.
westurner 5y ago
From "Discover and Prevent Linux Kernel Zero-Day Exploit Using Formal Verification" https://news.ycombinator.com/item?id=27442273 https://news.ycombinator.com/item?id=27442273 : > [Coq, VST, CompCert] > Formal methods: https://en.wikipedia.org/wiki/Formal_methods https://en.wikipedia.org/wiki/Formal_methods > Formal specification: https://en.wikipedia.org/wiki/Formal_specification https://en.wikipedia.org/wiki/Formal_specification > Implementation of formal specification: https://en.wikipedia.org/wiki/Anti-pattern#Software_engineering https://en.wikipedia.org/wiki/Anti-pattern#Software_engineer... > Formal verification: https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification > From "Why Don't People Use Formal Methods?" https://news.ycombinator.com/item?id=18965964 https://news.ycombinator.com/item?id=18965964 : >> Which universities teach formal methods? >> - q=formal+verification https://www.class-central.com/search?q=formal+verification https://www.class-central.com/search?q=formal+verification >> - q=formal+methods https://www.class-central.com/search?q=formal+methods https://www.class-central.com/search?q=formal+methods >> Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs?
tombert 5y ago
I agree; I've been trying to get employers/coworkers to look into TLA+ or Isabelle (for different things) for years now, and it feels like only after every cryptocurrency started blogging did they start to listen. I find it funny that the reason we want the cryptocurrencies to be formally verified is because we want rock-solid financial transactions so that this distributed story is always accurate (which is good), but actual banks don't seem to have these same requirements. NOTE: Could be wrong on that last point, getting my information about banks third-hand, it's possible that banks are using formal verification. Can someone who works at a bank confirm?
- WanderPanda 5y ago
  Banks have the global exception handling system called courts to fall back to, tough.
  - tombert 5y ago
    Yeah, which always felt like that would be a great reason to formally verify...If a race condition ends up draining my account of all my money, you can bet that I am going to sue for the lost funds and probably a bunch of other things, which I cannot imagine would be very cheap for the bank. In fact, I would think it would be expensive for them even if it wasn't their fault (e.g. maybe there was no money in my account because I just have bad spending habits and a bad memory). It seems to me that having every bit of evidence on their end to prove that they are guaranteeing our transactions would be a really good thing....I suppose this solution might just work itself out if banks actually start relying on some kind blockchain to secure their transactions.
    - vineyardmike 5y ago
      > which I cannot imagine would be very cheap for the bank Its cheaper for everyone for them to say oops and give you the money back. Its more expensive for you to sue than for them to be sued.
- lottin 5y ago
  This is because banks rely on property rights, which are enforced by courts, whereas cryptocurrencies operate on a "fait accompli" basis (i.e. whoever happens to control the coins, owns them). This means, in the cryptocurrency world, mistakes are irreversible. In conventional finance, this is not usually the case.
serverholic 5y ago
Despite all the drama around crypto, there is a lot of cool stuff going on in that space.

You know, I'm not really into cryptocurrency, but it does seem like it's contributing to a resurgence of interest in formal methods. So - thank you, cryptocurrency community!

galangalalgol 5y ago

I've worked on safety critical software, but we did not use formal methods. Lots of test and checking for coverage (at asm level). Oodles of static analysis and wading through false positives. Do formal methods usually supplement those or replace some of it? Can provers or formal methodologies scale to safety critical codebases of 100s of ksloc? Whether such codebases should exist, or be better partitioned is a separate issue.

notimrelakatos 5y ago
Formal methods seems to be perfect for verifying protocols, specially finding design flaws, here an example of an ongoing effort to verify TLS https://www.mitls.org/ https://www.mitls.org/ https://github.com/project-everest/mitls-fstar https://github.com/project-everest/mitls-fstar
someguyorother 5y ago
The current crowning achievement of formal methods is, as I understand it, seL4. It is a formally proven microkernel of about 8500 LOC. There's still a while to go until they can scale to 100kLOCs, unfortunately.
- nextaccountic 5y ago
  CompCert is also very impressive. It's not, however, free software / open source (the source is available though) https://www.absint.com/compcert/structure.htm https://www.absint.com/compcert/structure.htm A problem with both seL4 and CompCert is that the code written to express the proofs is huge, much larger than code that actually does stuff. This puts a ceiling on the size of the projects we can verify. F* is a language that tries to address that, by finding proofs with z3, a smt prover; z3 can't prove everything on its own but it cuts down proof code by orders of magnitude. They have written a verified cryptography stack and TLS stack, and want to write a whole verified http stack. https://www.fstar-lang.org/ https://www.fstar-lang.org/ https://github.com/project-everest/hacl-star https://github.com/project-everest/hacl-star https://www.mitls.org/ https://www.mitls.org/ https://project-everest.github.io/ https://project-everest.github.io/ F* (through Low, a verified low-level subset of F) can extract verified code to C, which is kind of the inverse than the seL4 proof: seL4 begins with C code and enriches it with proofs of correctness; hacl* (a verified crypto F* lib) begins with a proven correct F* code and extracts C code (I gather the actual crypto primitives is compiled directly to asm code because C has some problems with constant time stuff). This enables hacl* to make bindings to other languages that can just call C code, like this Rust binding https://github.com/franziskuskiefer/evercrypt-rust https://github.com/franziskuskiefer/evercrypt-rust Also this F* stuff is all free software / open source, so it might become a very prevalent crypto and TLS stack
retrac 5y ago
Not as a monolithic object. You might be able to do it with an almost microkernel approach (whatever you're implementing) with multiple small, well-defined objects with a well-defined protocol between them. That can be very useful. But I doubt you could formally verify their collective behaviour. The space and time complexity of the algorithms is explosive as the number of interacting objects increases.
- maweki 5y ago
  Note that the specification (what you prove correctness of the implementation against) already grows with the number of interactions.
tombert 5y ago
I've never really worked on anything safety-critical, but I know that at least one real-time operating has been designed and verified with TLA+ [1]. The book is a bit pricey (and used copies don't pop up that often), so I haven't read it, but my understanding is that the developers felt that TLA+ did find bugs. That said, TLA+ is written separately from the code. There could of course be bugs in the translation of TLA+ -> C...TLA+ is about checking the design itself, not the code. [1] https://www.springer.com/gp/book/9781441997357 https://www.springer.com/gp/book/9781441997357
noneeeed 5y ago
Yes, they are normally used in conjunction with testing. But they are also used in conjunction with careful systems engineering to minimise the amount of code that needs to go through the most rigerous processes and focus on what really mattered. I'm curious which static analysis tool you were using. I used to work in SPARK Ada and false positives were not really a thing due to how it worked. But I've heard of others that were much less restrictive which ended up with lots of false positives, or "maybe" cases that then wasted everyone's time. I can see how systems like that would put people right off using them.
diroussel 5y ago
AWS have worked with Leslie Lamport of proving properties about S3. See: Use of Formal Methods at Amazon Web Services https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....

X6S1x6Okd1st 5y ago

Another public good that cryptocurrency has been contributing to is advances in zero knowledge proofs including some really interesting stuff like SNARKs

tromp 5y ago
Here's the state of the art on that: https://iacr.org/cryptodb/data/paper.php?pubkey=31249 https://iacr.org/cryptodb/data/paper.php?pubkey=31249
- X6S1x6Okd1st 5y ago
  One thing to highlight how important this may turn out to be: > Proof-carrying data (PCD) enables a set of parties to carry out an indefinitely long distributed computation where every step along the way is accompanied by a proof of correctness. It generalizes incrementally verifiable computation This has the potential to remove the element of trust that you currently must place in the provider of computation resources. With SNARKs you can simply ask them to include a proof that they actually performed the computation that is sublinear in the length of the proof and sublinear in the amount of time taken to verify the proof. Of course this will always be more computationally expensive for the provider of the computation resources to both do the work and provide the proof.
miketery 5y ago
Any good tutorials? I’m having a hard time understanding some of the write ups I’ve found so far.

yjftsjthsd-h 5y ago

It also seems associated with advances in wider adoption and some progression in state of the art of functional package managers and reproducible builds, which has been nice to see.

westurner 5y ago

From "Discover and Prevent Linux Kernel Zero-Day Exploit Using Formal Verification" https://news.ycombinator.com/item?id=27442273 https://news.ycombinator.com/item?id=27442273 : > [Coq, VST, CompCert] > Formal methods: https://en.wikipedia.org/wiki/Formal_methods https://en.wikipedia.org/wiki/Formal_methods > Formal specification: https://en.wikipedia.org/wiki/Formal_specification https://en.wikipedia.org/wiki/Formal_specification > Implementation of formal specification: https://en.wikipedia.org/wiki/Anti-pattern#Software_engineering https://en.wikipedia.org/wiki/Anti-pattern#Software_engineer... > Formal verification: https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification > From "Why Don't People Use Formal Methods?" https://news.ycombinator.com/item?id=18965964 https://news.ycombinator.com/item?id=18965964 : >> Which universities teach formal methods? >> - q=formal+verification https://www.class-central.com/search?q=formal+verification https://www.class-central.com/search?q=formal+verification >> - q=formal+methods https://www.class-central.com/search?q=formal+methods https://www.class-central.com/search?q=formal+methods >> Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs?

tombert 5y ago

I agree; I've been trying to get employers/coworkers to look into TLA+ or Isabelle (for different things) for years now, and it feels like only after every cryptocurrency started blogging did they start to listen. I find it funny that the reason we want the cryptocurrencies to be formally verified is because we want rock-solid financial transactions so that this distributed story is always accurate (which is good), but actual banks don't seem to have these same requirements. NOTE: Could be wrong on that last point, getting my information about banks third-hand, it's possible that banks are using formal verification. Can someone who works at a bank confirm?

WanderPanda 5y ago
Banks have the global exception handling system called courts to fall back to, tough.
- tombert 5y ago
  Yeah, which always felt like that would be a great reason to formally verify...If a race condition ends up draining my account of all my money, you can bet that I am going to sue for the lost funds and probably a bunch of other things, which I cannot imagine would be very cheap for the bank. In fact, I would think it would be expensive for them even if it wasn't their fault (e.g. maybe there was no money in my account because I just have bad spending habits and a bad memory). It seems to me that having every bit of evidence on their end to prove that they are guaranteeing our transactions would be a really good thing....I suppose this solution might just work itself out if banks actually start relying on some kind blockchain to secure their transactions.
  - vineyardmike 5y ago
    > which I cannot imagine would be very cheap for the bank Its cheaper for everyone for them to say oops and give you the money back. Its more expensive for you to sue than for them to be sued.
lottin 5y ago
This is because banks rely on property rights, which are enforced by courts, whereas cryptocurrencies operate on a "fait accompli" basis (i.e. whoever happens to control the coins, owns them). This means, in the cryptocurrency world, mistakes are irreversible. In conventional finance, this is not usually the case.

serverholic 5y ago

Despite all the drama around crypto, there is a lot of cool stuff going on in that space.