3 ms·

I hope that one of these days (years?) we might start seeing formally verified versions of code for dealing with standards that don't change rapidly and that ha

I hope that one of these days (years?) we might start seeing formally verified versions of code for dealing with standards that don't change rapidly and that have proved to be security problems in the past. I'm thinking of things like font rasterizers, TIFF readers, full PDF readers, and JavaScript engines intended for browsers.

nickpsecurity 10y ago
The problem with many of these formats is they're Turing-Complete languages with input driving what they do. The input is also malicious. So, the solution so far is to isolate and mediate such things with verification going into the mechanisms for that. An example of one for exactly your types of programs is Microsoft's Xax: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/xax-osdi08.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... My preferred approach is the old-school method of highly-assured microkernels that just separate everything else from one another. Here's a browser OS based on that principle: https://www.usenix.org/legacy/event/osdi10/tech/full_papers/Tang.pdf https://www.usenix.org/legacy/event/osdi10/tech/full_papers/...
- sliverstorm 10y ago
  Aren't microprocessors Turing-Complete machines that undergo formal verification?
  - nickpsecurity 10y ago
    The kind of verification they undergo varies considerably. The amount of errata in modern CPU's shows both they're not fully verified for correctness and that the verification they get works wonders given number of components & interactions. Even if fully verified, the verification would be that the Turing-Complete hardware properly implemented a model of the Turing-Complete hardware. That kind of buys us nothing in terms of whether we'll know if programs are malicious or contain them, eh? And look at the giant, losing game that followed between the mice and the well-fed cats. It's why safety-critical systems often used deterministic, state-machines running on simple MCU's or PLC's. :)
nabla9 10y ago
In the examples you mention (document readers) the bugs become security problems because programs have too much privileges. Easiest way to remove security problems is not to remove bugs, but remove privileges. Privilege revocation, privilege separation, W^X work wonders. Protocols like https, ssl and cryptography and operating systems would be my first choices.

nickpsecurity 10y ago

The problem with many of these formats is they're Turing-Complete languages with input driving what they do. The input is also malicious. So, the solution so far is to isolate and mediate such things with verification going into the mechanisms for that. An example of one for exactly your types of programs is Microsoft's Xax: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/xax-osdi08.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... My preferred approach is the old-school method of highly-assured microkernels that just separate everything else from one another. Here's a browser OS based on that principle: https://www.usenix.org/legacy/event/osdi10/tech/full_papers/Tang.pdf https://www.usenix.org/legacy/event/osdi10/tech/full_papers/...

sliverstorm 10y ago
Aren't microprocessors Turing-Complete machines that undergo formal verification?
- nickpsecurity 10y ago
  The kind of verification they undergo varies considerably. The amount of errata in modern CPU's shows both they're not fully verified for correctness and that the verification they get works wonders given number of components & interactions. Even if fully verified, the verification would be that the Turing-Complete hardware properly implemented a model of the Turing-Complete hardware. That kind of buys us nothing in terms of whether we'll know if programs are malicious or contain them, eh? And look at the giant, losing game that followed between the mice and the well-fed cats. It's why safety-critical systems often used deterministic, state-machines running on simple MCU's or PLC's. :)

nabla9 10y ago

In the examples you mention (document readers) the bugs become security problems because programs have too much privileges. Easiest way to remove security problems is not to remove bugs, but remove privileges. Privilege revocation, privilege separation, W^X work wonders. Protocols like https, ssl and cryptography and operating systems would be my first choices.