lkml.org 
[lkml]   [1998]   [Aug]   [30]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: Virtual Machines, JVM in kernel, hot-swapped kernel
On Sat, Aug 29, 1998 at 08:09:36PM -0300, Brandon S. Allbery KF8NH wrote:
>
> Code produced by a designated compiler might be safe, but if you're loading
> native code (i.e. the compiler isn't in the kernel) then it would be
> possible to load arbitrary code. This would not be possible if the kernel
> used a bytecode interpreter with restricted operations (file ops would not
> be wanted or needed for this, for instance, nor would arbitrary pointer ops).
>
> JIT wouldn't suffer from this (modulo bugs), but it *would* have a
> significantly larger footprint. I don't think that is a very good idea,
> either, especially since it wouldn't be pageable code.
>

I was thinking of a in-kernel jit-compiler. My point is that you get
significant speed improvements by using a simple table-driven jit. A
table-driven jit is very simple - it works by reading one byte-code
and producing 2-3 native instructions. It could probably be
implemented in a page.

> | An alternative if you want even better performance is to look into
> | Proof-Carrying-Code which means that instead of having a JIT in the
> | kernel, you have a proof-verifier. Instead of byte code you use
> +--->8
>
> A certain Knuth quote springs to mind. And if the proof verifier were
> np-complete (wouldn't it have to be?), it would present still another way to
> hang a system inadvertently. (I ignore deliberate attacks because anyone
> able to do so could just as easily insmod a killer module, not to mention
> any number of other nasties possible to someone with root access.)
>

Verifying isn't np-complete. User-level has to explain to the kernel
why a particular piece of code is safe. The kernel is just verifying
that the proof is correct. I think a verifyer is quite simple.

Proving that the code is correct is the hard part (np-complete), but a
user-level problem. But if I remember correctly, it is possible to
automate the process for limited problems such as packet-filters.

PCC might be a research area right now, but it seems to be close
enough to be implementable if someone put their mind to it. Here are
some papers on PCC.


@InProceedings{POPL::Necula1997,
title = "Proof-Carrying Code",
author = "George C. Necula",
pages = "106--119",
booktitle = "Conference Record of {POPL}~'97: The 24th {ACM}
{SIGPLAN}-{SIGACT} Symposium on Principles of
Programming Languages",
month = "15--17 " # jan,
year = "1997",
address = "Paris, France",
references = "\cite{JACM::BoyerY1996} \cite{JACM::HarperHP1993}
\cite{APAL::MillerNPS1991} \cite{LICS::Pfenning1989}",
}

@InProceedings{NecLee98,
author = "G. C. Necula and P. Lee",
title = "Safe, Untrusted Agents using Proof-Carrying Code",
booktitle = "Mobile Agents and Security",
volume = "1419",
year = "1998",
publisher = "SV",
series = "LNCS",
editor = "G. Vigna",
added-at = "Mon Mar 30 11:47:35 1998",
abstract = "This paper is intended to be both a comprehensive
implementation guide for a Proof-Carrying Code system
and a case study for using PCC in a mobile agent
environment. Specifically, the paper describes the use
of PCC for enforcing memory safety, access control and
resource usage bounds for untrusted agents that access
a database.",
on-line = "http://www.cs.cmu.edu/~necula/lncs98.ps.gz",
booktitle = "Safe, Untrusted Agents using Proof-Carrying Code",
}


@InProceedings{Necula97,
author = "G. C. Necula",
title = "Proof-carrying code",
address = "Paris, France",
year = "1997",
month = jan,
pages = "106--119",
booktitle = "Proceedings of the 24th {ACM} Symposium on Principles
of Programming Languages ({POPL'97})",
url = "http://www.cs.cmu.edu/~necula/popl97.ps.gz",
}


@InProceedings{NeculaLee98,
author = "G. C. Necula and P. Lee",
title = "The Design and Implementation of a Certifying
Compiler",
year = "1998",
added-at = "Mon Mar 30 12:08:16 1998",
abstract = "This paper presents a compiler from a type-safe subset
of the C language to optimized DEC Alpha machine code.
The novel feature of the compiler is that it contains a
certifier that automatically checks the type safety and
memory safety of any assembly language program produced
by the compiler. The result of the certifier is either
a formal proof of type safety or a counterexample
pointing to a potential violation of the type system by
the assembly-language target program. The ensemble of
the compiler and the certifier is called a certifying
compiler. Several advantages of certifying compilation
over previous approaches can be claimed. The notion of
a certifying compiler is significantly easier to employ
than a formal compiler verification, in part because it
is generally easier to verify the correctness of the
result of a computation than to prove the correctness
of the computation itself. Also, the approach can be
applied even to highly optimizing compilers, as
demonstrated by the fact that our compiler generates
target code, for a range of realistic C programs, which
is competitive with both the cc and gcc compilers with
all optimizations enabled. The certifier also
drastically improves the effectiveness of compiler
testing because, for each test case, it statically
signals compilation errors that might otherwise require
many executions to detect. Finally, this approach is a
practical way to produce the safety proofs for a
Proof-Carrying Code system, and thus may be useful in a
system for safe mobile code.",
booktitle = "PLDI'98",
url = "http://www.cs.cmu.edu/~necula/pldi98.ps.gz",
}


> | US citizens might want to look into their
> | "byte-code-in-the-kernel"-patent.
>
> !!! Wouldn't the BPF constitute prior art?
>

I'm not a lawyer and not a US citizen :-)

astor

--
Alexander Kjeldaas, Guardian Networks AS, Trondheim, Norway
http://www.guardian.no/

-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu
Please read the FAQ at http://www.altern.org/andrebalsa/doc/lkml-faq.html

\
 
 \ /
  Last update: 2005-03-22 13:44    [W:1.389 / U:0.712 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site