4 ms·

I'd like to see the industry move towards proof-carrying code. This takes decideability checking one step farther: not only does your driver have to be decideab

I'd like to see the industry move towards proof-carrying code. This takes decideability checking one step farther: not only does your driver have to be decideable, you have to prove that ahead of time and include a proof that can be checked in linear-time right along with the binary. At that point even signatures become redundant; you don't need to trust any central authority if you have proof of the programs validity right there.

Animats 5y ago
You still need some criterion to verify against. The Static Driver Verifier is successful because its criterion is just "will not blither all over memory" or make an incorrect API call. Passing the check doesn't mean the driver will drive the device properly, but it shouldn't crash the kernel. Or offer buffer overflow exploits.
- Joker_vD 5y ago
  Yes, those exactly are criteria that PCC was developed in mind with: "examples of safety properties that are covered in this paper are memory safety and compliance with data access policies, resource usage bounds, and data abstraction boundaries" (from the abstract of [0]). That's what safety is, after all: that something bad does not happen. [0] George C. Necula, Peter Lee. Safe, Untrusted Agents using Proof-Carrying Code. 1998. http://www.cs.cmu.edu/afs/cs/project/pop-10/member/petel/www/publications/lncs98.pdf http://www.cs.cmu.edu/afs/cs/project/pop-10/member/petel/www...
- daxfohl 5y ago
  Isn't Microsoft still trying to make a proven TLS implementation? If that takes really smart people years and years to do, I don't see much hope for the rest of us on line of business apps.
- infogulch 5y ago
  Yes, choosing the right criteria / spec to prove against is a big task, and one that is not done at all today. Mathematicians sometimes say that fully describing the problem can be more work than actually proving it with a particular solution, and I imagine there's some parallels between that and the criteria vs proof problem you mention here. If there's a biggest problem it's that nobody cares about a good spec so nobody will pay for it.
pjmlp 5y ago
For that to happen the industry needs to care more about quality, and that will only happen when liability becomes a real thing across the industry and not only in highly critical software.

Animats 5y ago

You still need some criterion to verify against. The Static Driver Verifier is successful because its criterion is just "will not blither all over memory" or make an incorrect API call. Passing the check doesn't mean the driver will drive the device properly, but it shouldn't crash the kernel. Or offer buffer overflow exploits.

Joker_vD 5y ago
Yes, those exactly are criteria that PCC was developed in mind with: "examples of safety properties that are covered in this paper are memory safety and compliance with data access policies, resource usage bounds, and data abstraction boundaries" (from the abstract of [0]). That's what safety is, after all: that something bad does not happen. [0] George C. Necula, Peter Lee. Safe, Untrusted Agents using Proof-Carrying Code. 1998. http://www.cs.cmu.edu/afs/cs/project/pop-10/member/petel/www/publications/lncs98.pdf http://www.cs.cmu.edu/afs/cs/project/pop-10/member/petel/www...
daxfohl 5y ago
Isn't Microsoft still trying to make a proven TLS implementation? If that takes really smart people years and years to do, I don't see much hope for the rest of us on line of business apps.
infogulch 5y ago
Yes, choosing the right criteria / spec to prove against is a big task, and one that is not done at all today. Mathematicians sometimes say that fully describing the problem can be more work than actually proving it with a particular solution, and I imagine there's some parallels between that and the criteria vs proof problem you mention here. If there's a biggest problem it's that nobody cares about a good spec so nobody will pay for it.

pjmlp 5y ago

For that to happen the industry needs to care more about quality, and that will only happen when liability becomes a real thing across the industry and not only in highly critical software.