Comment by nickpsecurity | Hacker News Reader

Comment by nickpsecurity | Hacker News Reader

This is an old problem solved dozens of ways that mainstream just refuses to deal with. The requirement is even standard for proprietary products going for DO-178B certification. I believe they do quite manual confirmation but automated exists. The solution is called certified compilation: the verifiable transformation of source into binaries. You break the process into a series of steps which each can be verified with the CST's/AST's handed from one to the next. You can implement the steps yourself or validate someone else's, even easier if it's a safe[r] language. Examples each using different methods are VLISP [1], FLINT [2], and CompCert C [3].

Running Debian through CompCert while putting more work into CompCert for portability and optimization is the easiest solution with long-term benefits. Performance will go up steadily. Bug count will go down steadily because that's what SML/Ocaml does. Code will be more readable. Repeat for most trusted tools to drive assurance up across the board.

If they don't want to do that, then the result will be something along lines of just having a bunch of people compile and sign the distro publishing signatures, etc. You will trust that they trusted whatever they all looked at. And anyone whose studied GCC's source, etc will know that basically means they all saw the same code. They'd have to understand it all to have known if there was a weakness introduced. They won't, use of C/C++ makes that harder, plenty of rope to hang one's self in any common action, and it's why those of us doing subversion-resistant development use languages like ML's or Oberon. FOSS needs to similarly transition toward safe, comprehensible tools that aren't backdoor generators just by architecture & language used.

Otherwise, all this talk of preventing subversion is just talk: they're going to get in. And if not subversion, the endless stream of 0-day's from the language and architectural choices will continue to do the job. A re-implementation of the TCB's of our systems is long overdue.

[1] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.51....

[2] http://flint.cs.yale.edu/flint/software.html

[3] http://compcert.inria.fr/

If I remember correctly the problem Thompson described is tougher to deal with than this. Yes, the CompCert compiler is certified, but the problem is that the compiler that bootstrapped CompCert may not be. If you use some compiler (let's call it gccb, for backdoored gcc) to bootstrap CompCert that outputs ccb (backdoored compcert). Now you recompile CompCert with ccb since CompCert is certified. This gets you a final version of CompCert compiled with a bootstrapped CompCert. So the process is gccb -> ccb -> cc. But then the backdoor has just been transmitted down the line to cc.

Edit: also I just looked and it appears that CompCert is written in OCaml. This doesn't substantively change anything above. It just means that rather than having a backdoored gcc you'd have a backdoored ocamlc.

Realistically the only way to truly assure that your compiler is not backdoored is by writing it yourself in assembly. But then, your assembler might be backdoored. So you need to write your own assembler in binary. But then your processor might be backdoored. So you need to design your own processor. And then you might be safe. Of course, if someone really cared enough to backdoor all that stuff, they'd probably just come after you with a rubber hose at that point. And I think that was the point Thompson was trying to make.

I cant remember Thompson's stuff: Im talking the general problem. You're correct in that my first step shifts the problem: does it on purpose. Here's what subversion resistant development takes: modular software with sensible interfaces: ability to understand code for human review (closer to algorithm the better); ability to understand compiler passes in isolation; ability to implement toolchain in language of choosing. There are existing flows like this as I illustrated. So, you use them and leverage diverse audience to check results. I mean, would you rather implement CompCert passes by hand or GCC even without optimizations? See the difference? ;)

Now, I did have a method to solve problem you're addressing. You implement an assembler first. Then a macro assembler with macro's for HLL primitives. You can use that immediately to jmplement certified compiler. Alternately, you can pick up Oberon report or Scheme book to implement that to get a true HLL plus compiler. Then you implememt the certified compiler with it. Comprehension, code complexity, and trust are kept manageable by building layer by layer. This, for productivity not security, is how Wirth and Carl first built Lilith then Oberon. Same method will work again and good that ML/Scheme/Oberon folks already gave us doc's plus code to use. Lets use them.

Yep, building up like that would work. Oberon if I recall correctly is pretty simple too (maybe ~20k LOC?) so that would actually be possible by a small team.

It has many times. Nice, LISP-style example that was recently on HN:

https://speakerdeck.com/nineties/creating-a-language-using-o...

Note: LISP/Scheme interpreters and processors with plenty of detail (including source) can be found with Google. Many implemented before 1990. Will run on cheap FPGA's or process nodes. Can take it all the way to hardware. ;)

The macro ASM can be built on something like P-code: an idealized, low-level machine easy to deploy on CISC and RISC architectures. A good example of how to bridge ASM and HLL's is Hyde's High Level Assembly:

http://www.plantation-productions.com/Webster/

The HLL, for non-LISP audience, can be Oberon with aid of Wirth's Compiler Construction book among other papers:

http://www.ethoberon.ethz.ch/WirthPubl/CBEAll.pdf

So, many possibilities. People just gotta use them. Build a LISP w/ macros to build everything else still seems to be easiest strategy. Esp as one can reuse code from textbooks unlikely to be subverted. Wirth's next best.

Reply on news.ycombinator.com