That linked article is from 2007. Interestingly, the stuff that the author mentions as useless (proof carrying code) is now basically The Way that developers handle code that has security, reliability, or robustness requirements.
- Microsoft has long used a formal driver verifier to prove liveness and protocol properties associated with device drivers
One amazing piece of work going on right now in compilers is by Xavier Leroy, who cares a lot about formally proving that your compiler and its optimizations respect the semantics of the language (i.e. that its execution on hardware is within the range of possible executions specified by the original input language). Without the decades of work on formalization, semantics work, theorem provers, etc. the community wouldn't have a chance of tackling those problems today.
Certainly, if you read the proceedings of POPL or even some ICFP papers, you might wonder where it's going. And even the authors might admit to the same. But until you've fully explored the issues that come up when you try to merge (shameless example from my own work) effect types, region types, concurrency, parallelism, and transactions, it's hard to know what sets of language features can be safely combined in a way that programmers can modularly reason about and a toolchain can implement efficiently and correctly.
I don't think what Native Client does is the same as "proof carrying code". From what I gather, if it used proof carrying code, then it would do some verification on the receiving side at "compile time", and no sandbox for runtime checks would be necessary.
My understanding is that Native Client works with a combination of a special compiler toolchain (on the sending side) and runtime checks on the receiving side.
You are correct --- PCC (AFAIK) has not come about in the sense of carrying along a proof object that a formal verifier can validate is both correct and corresponds to the code payload.
As the other commenter pointed out, the SLAM tools are part of the Windows Device Driver Development Kit. The last time I talked to the kit's dev manager (~2003), they were talking about making it mandatory that you pass the formal verification in order to have your driver signed by Microsoft. Since those signatures are then verified at driver installation time, that feels very close to it!
I have to confess I'm only familiar with the publications on Native Client and not the actual product. From what I'd read, I understood that the verifier did some basic static analysis to prove that all possible executions did not validate some properties. In that case, no proof object is required, as the source code itself is the proof object. Assuming, of course, that they're actually doing the stuff talked about in the papers and in practice don't just "grep for dangerous instructions."
- For example, Google Native Client uses a formal verifier to prove the safety of binaries (http://sos.cse.lehigh.edu/gonative/index.html )
- Microsoft has long used a formal driver verifier to prove liveness and protocol properties associated with device drivers
One amazing piece of work going on right now in compilers is by Xavier Leroy, who cares a lot about formally proving that your compiler and its optimizations respect the semantics of the language (i.e. that its execution on hardware is within the range of possible executions specified by the original input language). Without the decades of work on formalization, semantics work, theorem provers, etc. the community wouldn't have a chance of tackling those problems today.
Certainly, if you read the proceedings of POPL or even some ICFP papers, you might wonder where it's going. And even the authors might admit to the same. But until you've fully explored the issues that come up when you try to merge (shameless example from my own work) effect types, region types, concurrency, parallelism, and transactions, it's hard to know what sets of language features can be safely combined in a way that programmers can modularly reason about and a toolchain can implement efficiently and correctly.