6 ms·

Self-insert time. I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the so

by m1el 2mo ago

Self-insert time. I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost. We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point) So the cost of finding and developing exploits has dropped dramatically. On the other hand, formal verification is now much easier, since LLMs can automate the proof. You don't even need to worry about hallucinations, you merely need to trust Lean core. If the LLM is wrong, the proof will get rejected! The problem of exploits gets bigger, and the solution of formal verification gets cheaper. As a result, the needle is now moving in the direction of "more formal verification". I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time. My (ambitious) goal is to have a self-hosting, formally verified compiler, which allows proof transfer from source code down to assembly. I have not achieved that goal yet. What I have so far: - one (non-optimized) compiler step which is formally verified - three simple functions (hex, hex with labels, strtoull) formally verified, against RISC-V assembly, and against a custom IR https://github.com/m1el/riscv-fv-bootstrap https://github.com/m1el/riscv-fv-bootstrap The project is in quite a bad shape, and I am trying to improve my skills in that direction.

logicchains 2mo ago
Have you heard of https://cakeml.org/ https://cakeml.org/? It's a self-hosting formally verified compiler.
- m1el 2mo ago
  Thank you, I've heard of it. It is indeed very close to what I want to have. CakeML project also has a language Pancake, which has interesting properties. Here's the list of projects which I'm aware of: https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/third-party https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/...
boccaff 2mo ago
Don't we still need to verify that what the LLM proved is actually the stated system?If agents cutting corners (like deleting tests) is a concern, how can we be sure that the verification corresponds to the software and that every _load bearing_ assumption is true? I don't think that simply trusting the Lean core is enough.
- kolinko 2mo ago
  Of course, and correct verification assumptions were always a challenge, and they are a possible failure point - but 95%(?) of labour was then proving the code, and now that part can be largely automated. Speaking of how difficult can it be to write a proper spec, I think a few years ago someone found a bug in spec in a helloworld-like example in a book about formal methods, and a bug in the code.
- jhanschoo 2mo ago
  While that is true, just having LLMs "think about it" may discover unintended behavior and exploits, and you can choose to what extent you want to verify that the claims are correct.
- andor 2mo ago
  The LLM does not prove anything (it cannot reason). It generates Lean code, and conveniently, in Lean, the code is also the proof. It’s not merely a model of the stated system, it is the system. You still need to verify that the generated code is what you asked for, though.
  - eru 2mo ago
    > The LLM does not prove anything (it cannot reason). What is that supposed to mean? > It generates Lean code, and conveniently, in Lean, the code is also the proof. It’s not merely a model of the stated system, it is the system. Yes, and that's great. (Though, of course, the computer doesn't execute lean directly, it gets translated first.) > You still need to verify that the generated code is what you asked for, though. Yes, but you only need to read the theorems, not the proofs nor code.
- 2mo ago
rurban 2mo ago
We do have formally verifying C and C++ compilers already. cbmc and esbmc.
hobofan 2mo ago
> I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time. I don't know. It seems to match the general futility of pedantry that exists in all professions. Yes, you can try to optimize for absolute 0 flaws in your code, but in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit silly beyond a certain point.
- thomasahle 2mo ago
  > in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit silly beyond a certain point CPUs are tested so so much more thoroughly than any software today. Including using formal proofs. If the chance of a CPU bug is something like 1/10^6 and each module in your software is 1/10, reducing that to 1/100 makes a bog difference.
  - hobofan 2mo ago
    > software is 1/10, reducing that to 1/100 makes a bog difference I fully agree! I'm all for moving the needle towards moving the needle towards more formal verification, but what GP is suggesting is full verification of programs, which is more akin to trying to achieve a 1/10^6 bug rate.
hajile 2mo ago
You formally verify that your incorrect solution executes without a hitch, but you might just be formally verifying that any user can hit your API and download all your plaintext passwords. Lots of security bugs are caused by incorrect specs from misunderstanding the problem and a formal verifier can’t fix these. Humans can’t think through every situation either (or the bugs wouldn’t exist) SMS that’s doubly true because NOBODY understands all the interactions of the system as a whole and how changes in the part they understand affect everything else. I’m not saying formal verification is bad, but it’s not a panacea and I’d wager would only fix a small percentage of existing bugs.
- im3w1l 2mo ago
  I think this is exactly it though. Instead of targeting the moving target of "correctness", we should be proving the absence of common defects. Proving that secrets CANNOT be downloaded is a very nice example actually: * Understandable * Portable across projects, you could imagine something like from specs import no_stealing_secrets no_stealing_secrets(secret_table) * Implicitly proves the absence of RCE, though I suppose it could allow something truly crazy like an interpreter that will run any attacker supplied program that can be proven not to steal the specified secrets
- m1el 2mo ago
  I understand that formal verification is not panacea. My issue is that the systems today can't even tell for certain "This network-connected program doesn't execute arbitrary code". We can have a common list of our demands to software. We can eliminate entire classes of issues. We can understand what the software does.
- deleted 2mo ago
  [deleted]
thaumasiotes 2mo ago
> We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point) But... if that's not the point, the claim is obviously untrue. The security industry includes public-facing bug bounty platforms. Those find far more vulnerabilities than Mythos ever will, if you're not even worried about what counts as a vulnerability.
empath75 2mo ago
I had claude spend about 2 hours friday modeling one of our kubernetes operators in TLA, and it found 8 bugs, including 2 that could cause data loss, and one of the other bugs was one we had been trying to figure out why it was happening for literally months.
nickpsecurity 2mo ago
There were many prototyoes of certifying compilers and proof-carrying code in academia. The FLINT group by themselves had many. Maybe try building on those.
- m1el 2mo ago
  Thank you for the suggestion, I will be sure to learn from those!
makira 2mo ago
This is great! Not sure which high level language you are targetting, but consider Subrust instead of C: https://github.com/orbitalhigh/subrust https://github.com/orbitalhigh/subrust How does LowIRSSA compare to P1pp from boot2 ?
- m1el 2mo ago
  LowIRSSA is very different from the SSA in the repo. LowIRSSA looks way more like SSA-WASM than assembly

by m1el 2mo ago

logicchains 2mo ago

Have you heard of https://cakeml.org/ https://cakeml.org/? It's a self-hosting formally verified compiler.

m1el 2mo ago
Thank you, I've heard of it. It is indeed very close to what I want to have. CakeML project also has a language Pancake, which has interesting properties. Here's the list of projects which I'm aware of: https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/third-party https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/...

boccaff 2mo ago

Don't we still need to verify that what the LLM proved is actually the stated system?If agents cutting corners (like deleting tests) is a concern, how can we be sure that the verification corresponds to the software and that every _load bearing_ assumption is true? I don't think that simply trusting the Lean core is enough.

kolinko 2mo ago
Of course, and correct verification assumptions were always a challenge, and they are a possible failure point - but 95%(?) of labour was then proving the code, and now that part can be largely automated. Speaking of how difficult can it be to write a proper spec, I think a few years ago someone found a bug in spec in a helloworld-like example in a book about formal methods, and a bug in the code.
jhanschoo 2mo ago
While that is true, just having LLMs "think about it" may discover unintended behavior and exploits, and you can choose to what extent you want to verify that the claims are correct.
andor 2mo ago
The LLM does not prove anything (it cannot reason). It generates Lean code, and conveniently, in Lean, the code is also the proof. It’s not merely a model of the stated system, it is the system. You still need to verify that the generated code is what you asked for, though.
- eru 2mo ago
  > The LLM does not prove anything (it cannot reason). What is that supposed to mean? > It generates Lean code, and conveniently, in Lean, the code is also the proof. It’s not merely a model of the stated system, it is the system. Yes, and that's great. (Though, of course, the computer doesn't execute lean directly, it gets translated first.) > You still need to verify that the generated code is what you asked for, though. Yes, but you only need to read the theorems, not the proofs nor code.
2mo ago

rurban 2mo ago

We do have formally verifying C and C++ compilers already. cbmc and esbmc.

hobofan 2mo ago

> I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time. I don't know. It seems to match the general futility of pedantry that exists in all professions. Yes, you can try to optimize for absolute 0 flaws in your code, but in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit silly beyond a certain point.

thomasahle 2mo ago
> in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit silly beyond a certain point CPUs are tested so so much more thoroughly than any software today. Including using formal proofs. If the chance of a CPU bug is something like 1/10^6 and each module in your software is 1/10, reducing that to 1/100 makes a bog difference.
- hobofan 2mo ago
  > software is 1/10, reducing that to 1/100 makes a bog difference I fully agree! I'm all for moving the needle towards moving the needle towards more formal verification, but what GP is suggesting is full verification of programs, which is more akin to trying to achieve a 1/10^6 bug rate.

hajile 2mo ago

You formally verify that your incorrect solution executes without a hitch, but you might just be formally verifying that any user can hit your API and download all your plaintext passwords. Lots of security bugs are caused by incorrect specs from misunderstanding the problem and a formal verifier can’t fix these. Humans can’t think through every situation either (or the bugs wouldn’t exist) SMS that’s doubly true because NOBODY understands all the interactions of the system as a whole and how changes in the part they understand affect everything else. I’m not saying formal verification is bad, but it’s not a panacea and I’d wager would only fix a small percentage of existing bugs.

im3w1l 2mo ago
I think this is exactly it though. Instead of targeting the moving target of "correctness", we should be proving the absence of common defects. Proving that secrets CANNOT be downloaded is a very nice example actually: * Understandable * Portable across projects, you could imagine something like from specs import no_stealing_secrets no_stealing_secrets(secret_table) * Implicitly proves the absence of RCE, though I suppose it could allow something truly crazy like an interpreter that will run any attacker supplied program that can be proven not to steal the specified secrets
m1el 2mo ago
I understand that formal verification is not panacea. My issue is that the systems today can't even tell for certain "This network-connected program doesn't execute arbitrary code". We can have a common list of our demands to software. We can eliminate entire classes of issues. We can understand what the software does.
deleted 2mo ago
[deleted]

thaumasiotes 2mo ago

> We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point) But... if that's not the point, the claim is obviously untrue. The security industry includes public-facing bug bounty platforms. Those find far more vulnerabilities than Mythos ever will, if you're not even worried about what counts as a vulnerability.

empath75 2mo ago

I had claude spend about 2 hours friday modeling one of our kubernetes operators in TLA, and it found 8 bugs, including 2 that could cause data loss, and one of the other bugs was one we had been trying to figure out why it was happening for literally months.

nickpsecurity 2mo ago

There were many prototyoes of certifying compilers and proof-carrying code in academia. The FLINT group by themselves had many. Maybe try building on those.

m1el 2mo ago
Thank you for the suggestion, I will be sure to learn from those!

makira 2mo ago

This is great! Not sure which high level language you are targetting, but consider Subrust instead of C: https://github.com/orbitalhigh/subrust https://github.com/orbitalhigh/subrust How does LowIRSSA compare to P1pp from boot2 ?

m1el 2mo ago
LowIRSSA is very different from the SSA in the repo. LowIRSSA looks way more like SSA-WASM than assembly