Re: Gödel and kernel backdoors

[Pavel Kankovsky <peak () argo troja mff cuni cz>]

On Sun, 19 Sep 2010, Georgi Guninski wrote:

> On Sun, Sep 19, 2010 at 06:21:35PM +0200, Pavel Kankovsky wrote:
> > On the other hand, It is possible to "detect all bad programs" if it is
> > allowed to err on the safe side and mistake some good programs for bad
> > programs. An extreme example is to call all programs bad unless their
> > exact code appears on the list of known good programs.
>
> i doubt this can be remotely implemented in practice because of dynamic
> code like |eval| and mobile code.

It certainly can be implemented. But it would be very restrictive. Perhaps
not quite convenient for a general purpose system but imho quite adequate
for systems whose task is to keep planes in the air, nuclear fuel in
reactor vessels etc. But keep reading...

> can |code| be realistically distinguished from |data| for current OSes
> (e.g. is a vim modeline *only a* plain string or a string + program) ?

Do it when it is unavoidable and do not do it when it is impossible.

The difference between "code" and "data" lies in their interpretation.
Is this e-mail message a piece of data or a piece of code executed by a
kind of virtual machine interpreting every byte of its body as an
instruction to display one character?

In fact, most of the "code" is not anything able to run on the top of 
bare metal. You need a (semi-)virtual machine implemented by an OS kernel 
that augments the CPU instruction set with system calls. And it is the 
ability to interact with the outer world via these system calls (or 
around them if kernel mechanisms can be circumvented) that really  
matters.

This leads us to an alternative approach: prove that 1. a certain virtual
machine will never make it possible to execute a "bad operation" (e.g.
modify the OS) and 2. the program cannot be executed by any other vm.
You do not need to care much about the actual program's code: it might
overwrite its machine code with input data, it might interpret and
evaluate the data as an expression in quantum lambda calculus or it might
attain sentience and examine them to find out the meaning of life or
whatever but it will never be able to do "bad things".


On Sun, 19 Sep 2010, Berend-Jan Wever wrote:

> nevermind the fact that a "good" program in your list may contain as yet
> unknown vulnerabilities which mean it's actually bad.

Although it is not possible to solve the general problem, it might be 
possible prove a certain property (such as the lack of security bugs)
for a given program (or a finite set of them).


On Sun, 19 Sep 2010, Christian Sciberras wrote:

> I'm afraid most of this talk is theoretical crap.

"Nazi science sneers at incompleteness theorems!"
Sorry, couldn't resist.

> There are no precise mathematics, in fact, all notion of probability is
> fragmenting so much, that the probability that anything happens nears
> to 1.

Mathematics is as precise as ever.
And people are as unable to grasp it as ever. :|


On Mon, 20 Sep 2010, Hurgel Bumpf wrote:

> In the end, the problem is on one side the os vendor bothering endusers
> with stupid stop signs that can be disabled with a simple click, and on
> the other side the user again, clicking on every accept button like a
> woodpecker.

Obviously, the real solution should make unsafe behaviour more difficult
for a user than safe behaviour.


On Mon, 20 Sep 2010 Valdis.Kletnieks () vt edu wrote:

> Godel, Turing, and all proved that you can't make that check 100% 
> correct. They said *nothing* about the possibility of building a checker   
> that's 99.99998% accurate (and in fact, that's totally within the realm
> of mathematical possibility).  There are *real* problems that Godel says
> *nothing* about but the real world does:

What is the meaning of these percents? Probability? Fraction?
99.99998 % is as good as zero (i.e. no good at all) if an adversary is
free to attack the remaining 0.00002 %.

Sun Tzu said it best: "The art of war teaches us to rely not on the
likelihood of the enemy's not coming, but on our own readiness to receive
him; not on the chance of his not attacking, but rather on the fact that
we have made our position unassailable."


On Mon, 20 Sep 2010, dave b wrote:

> News flash: Computers are just not secure enough for us to use.

This is very old news.

> But, I don't use computers ... only non-deterministic Turing machines ;)

Oh. Can I rent one millionth part of your tape? :)


-- 
Pavel Kankovsky aka Peak                          / Jeremiah 9:21        \
"For death is come up into our MS Windows(tm)..." \ 21st century edition /



_______________________________________________
Full-Disclosure - We believe in it.
Charter: http://lists.grok.org.uk/full-disclosure-charter.html
Hosted and sponsored by Secunia - http://secunia.com/