4 ms·

I think a lot of people are mis-seeing these Pegasus attacks as a problem of political will ("we need sanctions on NSO/Israel!") or memory safety ("rewrite it i

I think a lot of people are mis-seeing these Pegasus attacks as a problem of political will ("we need sanctions on NSO/Israel!") or memory safety ("rewrite it in Rust!") when there is a deeper problem: parser complexity. Specifically, we're using context-sensitive and Turing-complete parsers up and down the software stack, which (at the Turing-complete level of complexity, says Gödel) guarantees that determined attackers can expect to discover an exploitable "weird machine." Folks should watch this panel and other talks by Meredith L. Patterson (co-collaborator and wife of the late Len Sassaman) and Sergey Bratus (previously at DARPA, now Dartmouth) to get a sense of the problem and the solution. https://youtu.be/8tAxHrntBJs?t=806 https://youtu.be/8tAxHrntBJs?t=806 These folks are saying that, just as the industry handled over-the-wire insecurity with TLS and e2ee (and not rolling our own crypto) we can handle device exploitability with well-described data and automated parser generation from those descriptions (and not rolling our own parsers, which these folks say should be verboten for the same reason as rolling one's own crypto: parsing is too hard for non-specialists to get right). Moreover, we don't have to redo the whole stack for it to be meaningful: big players can start using this tooling (e.g. https://github.com/UpstandingHackers/hammer https://github.com/UpstandingHackers/hammer) for parsers handling data from very untrustworthy inputs, such as message payloads sent to a phone number. Apple's Lockdown mode is a step in this direction, though in such a crude, "burn the village" way that it makes the phone almost unusable. But sacrificing usability shouldn't be necessary with current methods. If these folks can make safe parsers for PDF (https://www.darpa.mil/program/safe-documents https://www.darpa.mil/program/safe-documents) it should be possible for anything. Another great talk: https://www.youtube.com/watch?v=3kEfedtQVOY https://www.youtube.com/watch?v=3kEfedtQVOY

divan 2y ago
Thank you for sharing these talks! I will never look at parsers the same way again.
hulitu 2y ago
> Pegasus attacks as a problem of political will ... when there is a deeper problem: parser complexity. There is a "problem of political will" but also the problem of stupid SW which tries very high to decode everything you throw at it. Some time ago it was "file format not recognized", nowadays it is a root exploit.
samatman 2y ago
You've over-egged the pudding here: neither Gödel's incompleteness theorem, nor Rice's Theorem, guarantee that an algorithm in a certain complexity class will have exploitable defect. Rice's Theorem in particular suggests that it's unlikely one will be able to statically prove that such an algorithm has the properties it's designed to have. That should be enough to make anyone nervous. I hope readers will be able to look past this one sentence in your post and take a good hard look at the rest of it, which is quite important.
- nextos 2y ago
  Rice's Theorem, as all Free Lunch Theorems, is too pessimistic. In real conditions, static analysis and theorem proving can verify lots of safety properties. See e.g. Astrée & Airbus, or F* and Project Everest. IMHO, the solution is to use static analysis in conjunction with DSLs that have restricted semantics to make static analysis and hand-written proofs easy.
  - samatman 2y ago
    It doesn't appear that we're disagreeing. You're referring to verifying 'lots' of safety properties, I referred to verifying that an algorithm does everything it's supposed to. These are not the same thing in the general case. My actual point was that generic incompleteness and undecidability theorems do not guarantee that any given program must be defective. The thrust of langsec is in fact to parse all inputs at the boundaries, using algorithms with known properties, that is, ones where it's feasible to prove that they'll halt, won't overrun buffers, and so on.
alephnerd 2y ago
The Gödel and computational complexity stuff is a bit out in the horizon, but the rest ain't wrong and is something that's getting a lot of (indirect) federal funding via the Secure Enclave/Trusted Execution Environment related research - and Bratus was one of the earlier people in the Trusted Computing space. > If these folks can make safe parsers for PDF (https://www.darpa.mil/program/safe-documents https://www.darpa.mil/program/safe-documents) it should be possible for anything It is, but it's very expensive. That's why a lot of this research has been getting billions in funding for 10-15 years now in order to build out the underlying ecosystem needed to harden the entire stack

divan 2y ago

Thank you for sharing these talks! I will never look at parsers the same way again.

hulitu 2y ago

> Pegasus attacks as a problem of political will ... when there is a deeper problem: parser complexity. There is a "problem of political will" but also the problem of stupid SW which tries very high to decode everything you throw at it. Some time ago it was "file format not recognized", nowadays it is a root exploit.

samatman 2y ago

You've over-egged the pudding here: neither Gödel's incompleteness theorem, nor Rice's Theorem, guarantee that an algorithm in a certain complexity class will have exploitable defect. Rice's Theorem in particular suggests that it's unlikely one will be able to statically prove that such an algorithm has the properties it's designed to have. That should be enough to make anyone nervous. I hope readers will be able to look past this one sentence in your post and take a good hard look at the rest of it, which is quite important.

nextos 2y ago
Rice's Theorem, as all Free Lunch Theorems, is too pessimistic. In real conditions, static analysis and theorem proving can verify lots of safety properties. See e.g. Astrée & Airbus, or F* and Project Everest. IMHO, the solution is to use static analysis in conjunction with DSLs that have restricted semantics to make static analysis and hand-written proofs easy.
- samatman 2y ago
  It doesn't appear that we're disagreeing. You're referring to verifying 'lots' of safety properties, I referred to verifying that an algorithm does everything it's supposed to. These are not the same thing in the general case. My actual point was that generic incompleteness and undecidability theorems do not guarantee that any given program must be defective. The thrust of langsec is in fact to parse all inputs at the boundaries, using algorithms with known properties, that is, ones where it's feasible to prove that they'll halt, won't overrun buffers, and so on.

alephnerd 2y ago

The Gödel and computational complexity stuff is a bit out in the horizon, but the rest ain't wrong and is something that's getting a lot of (indirect) federal funding via the Secure Enclave/Trusted Execution Environment related research - and Bratus was one of the earlier people in the Trusted Computing space. > If these folks can make safe parsers for PDF (https://www.darpa.mil/program/safe-documents https://www.darpa.mil/program/safe-documents) it should be possible for anything It is, but it's very expensive. That's why a lot of this research has been getting billions in funding for 10-15 years now in order to build out the underlying ecosystem needed to harden the entire stack