Messages in this thread | | | Date | Sun, 30 Aug 1998 18:22:15 +0200 | From | Alexander Kjeldaas <> | Subject | Re: 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
| |