> The funny thing about compiler optimization is, you're trying to make > a transformation that's valid for all possible input states, and > that's the security problem to begin with - your software works for > enough input states to pass muster, but not for every input state, and > a clever enough person can find the one where it works in their favor.
Have you seen http://www.cis.upenn.edu/~stevez/vellvm/ or http://compcert.inria.fr or https://www.usenix.org/node/186162 ? The compiler and verification community has done this, or things like it, before. VeLLVM is at a kind of different level than a "boring C" because you still need to translate the C AST into LLVM, but once you're there, we know how to do verified optimizations. The verified LLVM transformations is a part of the deepspec project (http://www.deepspec.org/) so that they can know that the assurances they make at the C or Haskell level carry through to the ISA. On 01/17/2016 02:09 AM, travis+ml-lang...@subspacefield.org wrote: > On Mon, Dec 21, 2015 at 10:21:21AM -0800, Will Sargent wrote: >> DJB on writing "boring" programs in C: >>> As a boring platform for the portable parts of boring crypto software, >>> I'd like to see a free C compiler that clearly defines, and permanently >>> commits to, carefully designed semantics for everything that's labeled >>> "undefined" or "unspecified" or "implementation-defined" in the C >>> "standard". This compiler will provide a comprehensible foundation for >>> people writing C code, for people auditing C code, and for people >>> formally verifying C code. >>> For comparison, gcc and clang both feel entitled to arbitrarily change >>> the behavior of "undefined" programs. Pretty much every real-world C >>> program is "undefined" according to the C "standard", and new compiler >>> "optimizations" often produce new security holes in the resulting object >>> code, as illustrated by >>> https://lwn.net/Articles/342330/ >>> https://kb.isc.org/article/AA-01167 >>> and many other examples. Crypto code isn't magically immune to this--- >>> one can easily see how today's crypto code audits will be compromised by >>> tomorrow's compiler optimizations, even if the code is slightly too >>> complicated for today's compilers to screw up. A boring C compiler will >>> eliminate these nasty surprises; it will prioritize predictability. >> >> >> https://groups.google.com/d/msg/boring-crypto/48qa1kWignU/o8GGp2K1DAAJ >> >> Will. > > So, he's asking for a completely specified C language, and a compiler > that implements it. Hmm. I thought the whole idea of leaving some of > the behaviors unspecified was to help with efficiency - but of course > the issue is, which behaviors? From a langsec POV, what do you do > with programs which rely on unspecified behavior? > > I've actually been predicting that faulty optimizations will be a very > fecund area of security research still. Nobody's really tapped into > it, but the point was driven home to me when BSDs started using egcs > to compile their userland and kernel. EGCS, if you remember, was the > enhanced gnu compiler suite, trying aggressive optimizations, and it > didn't work out very well in the early stages, although it's not clear > from the public history: > > https://www.gnu.org/software/gcc/egcs-1.1/ > http://www.softpanorama.org/People/Stallman/history_of_gcc_development.shtml > > The funny thing about compiler optimization is, you're trying to make > a transformation that's valid for all possible input states, and > that's the security problem to begin with - your software works for > enough input states to pass muster, but not for every input state, and > a clever enough person can find the one where it works in their favor. > > On top of that there's plenty of NPC problems in optimization. While > not strictly a correctness problem it's an interesting challenge. It's > too bad they don't memoize the correct solutions in a global db. That > could be our next block chain, and the next mining problem instead of > partial hash preimage brute forcing. > _______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
