Randomizing snake-oil

Posted May 12, 2017 7:38 UTC (Fri) by nhippi (subscriber, #34640)
Parent article: Randomizing structure layout

It is unfortunate security developers focus on probabilistic runtime defenses. The added complexity can easily become an attack surface itself. Making the code harder to understand and debug will inevitably create new bugs - some which will have security implications. I take working on better static checks (and integrating them into developer/maintainer workflow) would have better long term effect. But that of cause doesn't make nice bullet points to marketing brochures like "randomized structs" may make...

to post comments

Randomizing snake-oil

Posted May 12, 2017 8:17 UTC (Fri) by matthias (subscriber, #94967) [Link] (5 responses)

Focusing only on probabilistic defences is certainly not good. But I do not see this happening. It is just one defence among many.

Certainly it would be better to just have provably secure code. But as the kernel is several orders of magnitude too large for proving its correctness, there have to be other measures.

Also I do not see, where this makes the code harder to understand. This change takes the right way of hiding the added complexity in the compiler (to be precise in a plugin). The visible changes in code mostly come down to some hints, where randomization is allowed or not allowed.

For debug it is a bit different. However, with proper support in the debugger, this should be no problem. The debugger should be able to decode randomized structs, if it has the necessary seed.

Both approaches have long term effects. Static analysis can prevent some bugs (not all of them unless we restrict to non Turing complete languages). Randomization can prevent bugs being exploited. This includes bugs in newly added code. Which has more effect is hard to tell.

Randomizing snake-oil

Posted May 12, 2017 14:07 UTC (Fri) by ebiederm (subscriber, #35028) [Link] (4 responses)

Provably secure is pretty much a non-starter as it requires a full and accurate theory of everything, and a proof the hardware you run on meets it's specification. Short of that you will have assumptions that may be wrong somewhere in your approach.

That said it is possible to manage the assumptions and prove certain properties about code. Which could in principle could close many lines of attack. The kernel deliberately does not implement any turning machines not even with eBPF so the halting problem should not be an issue.

The practical problem and what most attacks today exploit is that to be able to reason soundly about logic or algorithms requires the abstractions you build those out of to be well defined. Currently C explicitly is not well defined with respect to memory management. When you add in devices that can perform DMA and are not restricted by an IOMMU (as a kernel must) there is an additional problem.

To my knowledge no one has yet demonstrated a system that can build operating systems that is sufficiently well defined as to allow proofs of correctness for anything interesting. Which unfortunately leaves proofs of correctness needing a proof of concept before anyone will believe in them.

Which is all to say people are adding kernel defenses some of the randomization because no one has been clever enough yet to think of something better.

Randomizing snake-oil

Posted May 12, 2017 18:40 UTC (Fri) by walters (subscriber, #7396) [Link]

https://sel4.systems/ is pretty interesting on this topic. That said, I thought Coccinelle was an intimidating but https://github.com/seL4/l4v/commit/df7693b687a5ad541d1bee... is totally unintelligible to me. (Why are there almost no comments?)

Randomizing snake-oil

Posted May 13, 2017 18:04 UTC (Sat) by NAR (subscriber, #1313) [Link] (1 responses)

"To my knowledge no one has yet demonstrated a system that can build operating systems that is sufficiently well defined as to allow proofs of correctness for anything interesting"

I remember 20 years ago someone mentioned to me that the VMS kernel (the OS running on VAX computers) was formally proven to be correct (to some degree). Of course, in that case DEC provided the hardware and the software too. Unfortunately I don't remember the details.

Randomizing snake-oil

Posted May 18, 2017 0:52 UTC (Thu) by smoogen (subscriber, #97) [Link]

I was told by a Dec guy was that the original story was that with the right assumptions you could make anything provably secure and then showed how it could be done with the VMS system. You basically start by assuming all sorts of things like not having an active attacker, a set of actions that the system will only do, dropping down all the hardware to the bare minimum etc etc. All of these are things that various "provable" had used in one set or another.. so why not put them all together. You basically had a brick with VMS installed on it, but it was provable that it was secure within the parameters that could be used.

The problem was that the joke got out hand as someone took it seriously and started passing around about how VMS was superior to Unix because it was provably secure.

How true this story is versus all the others... I don't know.

Randomizing snake-oil

Posted May 25, 2017 20:47 UTC (Thu) by Wol (subscriber, #4433) [Link]

> Provably secure is pretty much a non-starter as it requires a full and accurate theory of everything, and a proof the hardware you run on meets it's specification. Short of that you will have assumptions that may be wrong somewhere in your approach.

A correctness proof is mathematics.

Hardware is reality.

Congratulations on finding a proof that reality and mathematics coincide ... :-)

Cheers,
Wol

Randomizing snake-oil

Posted May 12, 2017 8:56 UTC (Fri) by aggelos (subscriber, #41752) [Link]

Actually solving problems is not in the interest of most people in the security field. Randomized defenses which "raise the bar", only to be conclusively shown inadequate within a few months are very convenient that way. This is a pattern both in academia and the industry. By pursuing defenses which cannot be complete (if you allow arbitrary programmer expressivity, you're always confronted with the halting problem), you keep the arms race going. This is to the benefit of both defenders and attackers (keeps the funds flowing).

Not being totally cynical about this, as of course "raising the bar" now is a consideration for many production deployments. In my (perhaps poorly informed) opinion though, the allocation of funds is clearly not concerned with eventually having robust solutions, just with piling complexity on top of complexity (academia is pretty good at that) with no end in sight.

And yes, there's no way to have flawless programs. Logic errors aside, even in a memory safe language, the programmers can very well implement their own instruction set and have a memory safety violation in their binary code (which would only be data to the type system). This is not really in the same class of "fundamentally unworkable" as expecting a huge source base to be kept bug free (see the recent kernel quotes of the week). This line of thought is a total derailment IMHO.