User: Password:
|
|
Subscribe / Log in / New account

Attacking hardened Linux systems with kernel JIT spraying

Attacking hardened Linux systems with kernel JIT spraying

Posted Nov 18, 2012 20:24 UTC (Sun) by deepfire (guest, #26138)
In reply to: Attacking hardened Linux systems with kernel JIT spraying by cyanit
Parent article: Attacking hardened Linux systems with kernel JIT spraying

Do you have ideas on how to accomplish this?

Do you argue against mechanisms to prevent exploitation until we do?

On what grounds?


(Log in to post comments)

Attacking hardened Linux systems with kernel JIT spraying

Posted Nov 19, 2012 11:37 UTC (Mon) by cyanit (guest, #86671) [Link]

Make the build fail unless the C code can be statically proved to have at least the same invariants that Java provides, plus ideally being deadlock-free, providing real-time response if desired, and other goodies.

Switch to an augmented version of the C language with annotations to help the theorem prover or to another existing language if it turns out to be necessary to be able to prove correctness.

Attacking hardened Linux systems with kernel JIT spraying

Posted Nov 19, 2012 13:24 UTC (Mon) by Wol (guest, #4433) [Link]

lol lol lol !!!

Good luck with ACHIEVING that!

It's a nice idea, but I guess the proof would take longer to run than the heat death of the universe, that is, if the proof itself doesn't contain bugs ...

The problem, as you seem to have missed, is that the kernel needs to be able to write to kernel memory ...

Cheers,
Wol

Attacking hardened Linux systems with kernel JIT spraying

Posted Nov 19, 2012 13:41 UTC (Mon) by cyanit (guest, #86671) [Link]

Well, if you wrote the kernel in a type-safe garbage-collected language (e.g. Java), then the static proof would be trivial since it is by construction impossible to violate the language invariants (assuming the VM and low-level support code is correct).

So, that's the solution if everything else fails.

Without garbage collection, you can still prove (with help from the programmer if needed) that everything is either reference counted with no cycles, pointed to by a single pointer with lifetime tied to the contained structure, or otherwise provide a proof that it is correctly handled.

Without full type safety, you can still prove, for instance, that memcpy only writes the (dst, dst + size) and that since dst points to an array of size, it is safe, and so on for more complex stuff.

The real reason is that apparently nobody cares enough to do the work.

Annotating the kernel to prevent exploits

Posted Nov 19, 2012 14:39 UTC (Mon) by ebiederm (subscriber, #35028) [Link]

A version of l4 has been proven so it is definitely possible.

The techniques and tools are not yet fully mature. So I would say that is a little more than lack of people caring that has not seen this happen. Especially when you are talking such a large code base.

I was playing with using frama-c which reportedly is one of the better frame works for connecting C code and a prover and it could not handle the C99 of my toy test program. Getting a tool like that to run successfully on the kernel source base with no annotations looks to be a significant undertaking.

Not that this problem is unique to tools like frama-c. Even the clang front end to llvm (an actual production c compiler) has has trouble building the linux kernel.

Annotating the kernel to prevent exploits

Posted Nov 19, 2012 22:39 UTC (Mon) by vonbrand (guest, #4458) [Link]

The seL4 is a microkernel, of which some 7500 lines of C code have been verified rigurously (assuming the compiler and the underlying machine are correct). That is many, many orders of magnitude away from even the most spartan Linux configuration.

state of the art in formal proofs of kernels

Posted Nov 20, 2012 4:26 UTC (Tue) by pjm (subscriber, #2080) [Link]

Even then, so far they only claim to have proven [subject to questionable assumptions such as the compiler conforming to the formalization that they've written themselves] that their C implementation has the same behaviour (and hence same set of bugs) as their implementation in a higher-level language. They haven't claimed to have proven anything (else) about the behaviour of that higher-level-language implementation. So for example, even if the seL4 microkernel contained a JIT compiler, they wouldn't have proven anything about the output of that compiler (to which the kernel presumably passes control while in kernel mode).

OTOH, that program equivalence would certainly reduce the opportunities for exploits (e.g. by ruling out any buffer overflows that don't occur in the higher-level language), and at least it's a bit easier to prove properties of code in a higher-level language than a lower-level one. Mathematical proofs increase confidence, but there's always a gap between a mathematical model and the real world.

state of the art in formal proofs of kernels

Posted Nov 20, 2012 11:45 UTC (Tue) by Cyberax (✭ supporter ✭, #52523) [Link]

There's research towards proving that compiler output is correct by using type-annotated assembly language. It might be actually possible to check whether high-level invariants are not mis-translated by the compiler.

The next frontier is to prove that hardware itself is correct :)

state of the art in formal proofs of kernels

Posted Nov 20, 2012 13:33 UTC (Tue) by ebiederm (subscriber, #35028) [Link]

There is compcert a formally proven C compiler written in coq.

Hardware design developed formal method for their logic ALUs and FPUs a long time ago. Although that clearly has it's limits. Especially timing.

The next frontier is for program proofs to stop being news and instead partial program proofs increasing program reliability to the point where any program updates except for features become news.

How we go from proofs of concept to useful proof tools is a question I don't yet see answers to.

state of the art in formal proofs of kernels

Posted Nov 20, 2012 19:14 UTC (Tue) by dlang (subscriber, #313) [Link]

> ...increasing program reliability to the point where any program updates except for features become news.

Given that people don't even bother to define what acceptable input is, I don't expect this to ever happen.

Not to mention that this would require anticipating all possible internal state, another thing that is not going to happen.

And then you need to have someone think through what should happen in all these combinations of cases, and not have any logic errors in what the 'proofs' are trying to show.

> Hardware design developed formal method for their logic ALUs and FPUs a long time ago. Although that clearly has it's limits. Especially timing.

And when Timing issues dominate, the 'correctness' generated by such proofs is pretty meaningless.

Math is not reality, they sometimes have a resemblance to each other, but that's just a happy coincidence.

Attacking hardened Linux systems with kernel JIT spraying

Posted Nov 19, 2012 16:00 UTC (Mon) by khim (subscriber, #9252) [Link]

Well, if you wrote the kernel in a type-safe garbage-collected language (e.g. Java), then the static proof would be trivial since it is by construction impossible to violate the language invariants (assuming the VM and low-level support code is correct).

Unfortunately this small addition at the end makes the whole thing useless: simple interpreter mode for languages like Java are too slow and thus "VM and low-level support code" is typically comparable in complexity to OS kernel (in some sense it is an OS kernel).

The real reason is that apparently nobody cares enough to do the work.

No. The real reason is that it takes time and does not pay.

Attacking hardened Linux systems with kernel JIT spraying

Posted Nov 19, 2012 16:40 UTC (Mon) by drag (subscriber, #31333) [Link]

It's better to have buggy code that works now then it is to have something that may work in 30 years.

Attacking hardened Linux systems with kernel JIT spraying

Posted Nov 20, 2012 3:07 UTC (Tue) by liam (subscriber, #84133) [Link]

Is there any reason why this work couldn't be done it parallel with kernel development?
There are parts of the kernel that are only touched rarely (ex. block/deadline-iosched, though there are probably better examples).
It seems as though this type of analysis might be good long term project.
Of course, if it is truly infeasible for any but the least interesting parts of the kernel then it is a waste of time.

Attacking hardened Linux systems with kernel JIT spraying

Posted Nov 20, 2012 19:15 UTC (Tue) by mathstuf (subscriber, #69389) [Link]

> Of course, if it is truly infeasible for any but the least interesting parts of the kernel then it is a waste of time.

I suppose that since there's a high chance of it happening, the question boils down to: "What wins when the decision is between ABI compatibility and provably secure?"

Attacking hardened Linux systems with kernel JIT spraying

Posted Nov 19, 2012 17:22 UTC (Mon) by NAR (subscriber, #1313) [Link]

Don't you think that assuming the VM and low-level support code is correct is a little too strong precondition?

The real reason is that apparently nobody cares enough to do the work.

I remember that back at the university proving that even a very simple concurrent program is correct took 30-40 minutes. And that model did not have shared memory or integer overflows...

Attacking hardened Linux systems with kernel JIT spraying

Posted Nov 20, 2012 8:55 UTC (Tue) by cmccabe (guest, #60281) [Link]

Have you been frozen in a cave for a few years? Java has been the subject of a bunch of zero-day vulnerabilities lately.

By all means, continue burbling on about the magical, deadlock-free, realtime, garbage collected in kernel space, 1000 miles-per-gallon programming language, but at least try to pretend that you read the article and/or recent news.

It's also funny that you're advocating using a (presumably JITed) garbage collected programming language in the kernel, and this vulnerability exploits the BPF JIT.

Being unfairly fair

Posted Nov 20, 2012 11:56 UTC (Tue) by man_ls (guest, #15091) [Link]

To be fair, this vulnerability exploits a combination of JIT and direct execution. If all kernel code was JITted with the same VM, then this kind of attack would be useless.

To be even fairer, to the point of unfairness, Java may have had vulnerabilities e.g. in executing protected code; but no buffer overflows. In C, every time a pointer is not checked for null before jumping, or an array index is not checked to be within bounds, there is an opportunity for a security vulnerability. I would trade 1000s of vulnerabilities for a handful any time, if it was even feasible to run a kernel in a VM.

In real life a kernel cannot run in a VM because it would need a kernel to run the VM -- or the VM would become the kernel. This is the way of the microkernel, which is slow. Embedding a VM inside another VM has no advantages and only slows things down even more.

On the other hand there is no reason why a kernel cannot be written in an object-oriented, reference-counted language. I have been thinking for a long time that it would be a worthwhile project, but for some reason have not found the time to do it in my spare time. Perhaps Golang would be a worthwhile instrument for the task.

a kernel cannot run in a VM

Posted Nov 20, 2012 21:46 UTC (Tue) by Wol (guest, #4433) [Link]

That was my immediate reaction.

Sorry to say it, but cyanit doesn't seem to understand the difference between a kernel and a VM.

A VM provides a *virtual* computer so that the programs don't need to give a fig what the real hardware is.

A kernel must interface directly with the hardware and cannot afford to ignore any figs.

Running a kernel in a VM is likely to vanish in a puff of smoke as it gets lost in a mobius loop!

Cheers,
Wol


Copyright © 2017, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds