Hacker News new | past | comments | ask | show | jobs | submit login

> You mean coding the stuff people are doing in LLVM and GCC in ML on CompCert or similar system?

No. I mean exactly what I said:

> I expect that the bar required to verify (or design and build from scratch) a high-performance optimizing compiler (and -in the case of systems with VMs- a high-performance VM) is substantially higher than the bar to rework your build system to give the same outputs for the same source code. [0]

Remember that this addressed your assertion that:

> None of [the projects doing reproducible builds] have verifiable builds. ... Verifiable builds are a larger problem they're ignoring because it's not a fad yet. [1][2]

If you can't see how my statement addresses the quoted claim, then more's the pity.

[0] https://news.ycombinator.com/item?id=11363783

[1] https://news.ycombinator.com/item?id=11362470

[2] Italics added for emphasis.




I may see what you're saying now. The problem is that this problem isnt solved in a vacuum: it's pre-requisites for security plus what SCM adds. They want to be sure the binary does what it's supposed to. That requires the What and How of source to be correct with no malicious modifications during development, storage, compilation, and distribution.

That's a large problem. The compiler part is smaller with lots of work in CompSci, FOSS, and private sector (eg books). There's tools with source available on net for imperative and functional languages that are safer, too. Ignored almost entirely by safety or security oriented projects in compilers and general FOSS in favor of harder-to-analyze, less secure stuff. However, they'll happily bring up fad-driven stuff like Thompson attack or reproducible builds as The Solution.

Here's the actual solution. You start with a simple, non-optimizing toolchain designed and documented for easy understanding and implementation. It has extensive test suite. User worried about subversion implements that in tooling of their choice on own machine. Wirth simplified it with P-code interpreter that was easy to inplement with compiler and apps targeting it. Once first compiler is done, it compiles the HLL source of its own code. Now, you can use it to compile a high-performance compiler's source or add optimizations to it. Most of this work is done so it's a natter of FOSS compiler types or project teams just integrating and using it.

They won't, though, because proven practices and components for secure, software engineering are rarely use. They do popular stuff instead which screws them up in other ways. At least the malicious or buggy source from the potentially subverted server run throigh a black box with similar issues has identical binary coming out. Take that NSA! ;)


> I may see what you're saying now.

To make sure that you do: It's obvious that you recognise the difficulty of creating a trustworthy compiler. Given that you have that information, it's rather disappointing that you chose to assert that this problem was being "ignor[ed] because it's not a fad yet".

> The problem is that this problem isnt solved in a vacuum...

That's one problem. Another problem is that the skills, competencies, and interests of one programmer differ (sometimes wildly) from that of another programmer.

Asserting that a randomly selected programmer isn't tackling the Verified Compiler problem just because it's not currently in vogue will likely be wrong as often as asserting that a randomly selected native Korean speaker doesn't also speak Greek because speaking Greek isn't currently in vogue.


"Given that you have that information, it's rather disappointing that you chose to assert that this problem was being "ignor[ed] because it's not a fad yet"."

This is one case among many. I counter it here all the time. There's literally dozens of works, including certification requirements, on securing this aspect of things. Yet, people have ignored all that from academia to industry every time we bring it up. Then, there's two things that pop up in every online discussion: Thompson attack or (recently) reproducible builds. Literally the smallest aspects of the problem with trusted distribution covered under old criteria. Why does that matter now but not before? It's a social phenomenon.

In 70's-80's, people designed, assured, and pentested guards with great results. Firewalls were a watered down version that came later with features but not assurance. Push guards on firewall proponents, even developers, then you'll just get ignored. They will work on whatever is making rounds on favorite IT or INFOSEC sites, though.

Compiler and OS people. They usually write their stuff in a monolithic style in C despite decades of bad results that way. Showing even one person (Edison), three (Lilith/Oberon), or handful (MINIX 3) can do entire system safer with less people and time will not change this. Showing them ML or something with C compilation for portability will not change this. They systematically reject this while doing whatever is their tradition or becomes in the vogue.

People making secure messaging apps have solid code and endpoint OS's to draw on. They rarely use them. They often use whatever most projects use or roll their own because it's fun. This is true even when shown risks, zero days, or benefits of alternatives.

All of these are social phenomenon that have nothing to do with technical difficulty. If anything, they're doing things that are harder to avoid the more robust option. This is systemic in our industry in compilers, OS's, and certain types of libraries. It's not about what a random Korean or Greek speaking programmer tackling a random project won't do. It's about the fact that almost all compiler-related work is ignoring the ways it got done robustly and more easily before. Same with SCM. There's exceptions, especially in functional, but the rule supports my point.

Most likely explanation for them chasing the same senseless stuff in mass even when shown evidence to the contrary... stuff that's easier... is that they chase fads for social reasons.




Join us for AI Startup School this June 16-17 in San Francisco!

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: