The Synthesis Kernel (1988) [pdf]
usenix.org
The Synthesis Kernel (1988) [pdf]
1–10 of 12 posts
Re: The Synthesis Kernel (1988) [pdf]
#2This paper was somewhat famous in the Berkeley system department when I was there; the lore was that it was the perfect academic system that proved a point but crashed ... frequently.
Re: The Synthesis Kernel (1988) [pdf]
#3Re: The Synthesis Kernel (1988) [pdf]
#4Mods: This needs a (1988)
Re: The Synthesis Kernel (1988) [pdf]
#5It says "Winter 1988"; the Morris Worm broke out in November that year. Security wouldn't really have been on people's minds so much yet. Which is perhaps why that word doesn't occur even once in this paper!
Clumsy system calls which start from first principles and traverse some data structures to get to the state they want can be verified for security issues. At every step they can validate each datum. For instance, a given integer file descriptor can not only become invalid between two successive read calls; it can point to a completely different object. We cannot cache/curry the resolution of that descriptor number to a descriptor object; we have to validate it from scratch on each call.
If you take any shortcuts via synthesized code or other tricks, you have to be able to convince yourself that security holes aren't created by skipping the sanity checks performed by the original system calls.
Re: The Synthesis Kernel (1988) [pdf]
#6ow! my eyes burn from the 80's texture background...
Synthesis was one of my favorite papers - sort of more Unixy, traditional-ish than Self (another fav from that decade...)
Re: The Synthesis Kernel (1988) [pdf]
#7It says "Winter 1988"; the Morris Worm broke out in November that year. Security wouldn't really have been on people's minds so much yet. Which is perhaps why that word doesn't occur even once in this paper! Clumsy system calls which start from first principles and traverse some data structures to get to the state they want can be verified for security issues. At every step they can validate each datum. For instance,…
If you can describe your synthesis operations in terms of some program transformation, you may be able to verify/prove that they preserve certain semantic properties (similar to compiler verification). We have both verified compilers and verified kernels already so this is not a long stretch but it would still be a research project of its own IMO. Also, there has been some research on breaking invariants temporarily between computational steps while preserving them overall [0] (unfortunately, behind a paywall and I couldn't find a non-paywall version).
My point is that although this paper doesn't discuss the security aspect, this work can be implemented in a secure manner.
Re: The Synthesis Kernel (1988) [pdf]
#8apparently Massalin is still at MicroUnity after 20 years. does anyone know if they do any business outside of patent licensing?
Re: The Synthesis Kernel (1988) [pdf]
#9It says "Winter 1988"; the Morris Worm broke out in November that year. Security wouldn't really have been on people's minds so much yet. Which is perhaps why that word doesn't occur even once in this paper! Clumsy system calls which start from first principles and traverse some data structures to get to the state they want can be verified for security issues. At every step they can validate each datum. For instance,…
If you can describe your synthesis operations in terms of some program transformation, you may be able to verify/prove that they preserve certain semantic properties (similar to compiler verification). We have both verified compilers and verified kernels already so this is not a long stretch but it would still be a research project of its own IMO. Also, there has been some research on breaking invariants temporarily…
You can just get it off Libgen as usual: http://dl.acm.org.sci-hub.io/citation.cfm?id=2661142
Re: The Synthesis Kernel (1988) [pdf]
#10It says "Winter 1988"; the Morris Worm broke out in November that year. Security wouldn't really have been on people's minds so much yet. Which is perhaps why that word doesn't occur even once in this paper! Clumsy system calls which start from first principles and traverse some data structures to get to the state they want can be verified for security issues. At every step they can validate each datum. For instance,…
If you can describe your synthesis operations in terms of some program transformation, you may be able to verify/prove that they preserve certain semantic properties (similar to compiler verification). We have both verified compilers and verified kernels already so this is not a long stretch but it would still be a research project of its own IMO. Also, there has been some research on breaking invariants temporarily…
It would have to be formally verified, because there is no informal way to have any confidence in this sort of thing.
The informal way is to have a team pore over code. Here, the body of code is some unbounded, dynamically generated set of little routines that are individually correct with respect to an unfolding run-time situation (not in and of themselves). Good luck, know what I mean?
If you log all the generated pieces of code, you don't know whether you have the whole set of them that can be. If not, there could be the bugs in the ones you don't have. Then there is the monstrous task of going through them, and somehow correlating each one to the situation that was unfolding (maybe with the help of additional logged information).
A static, monolithic piece of code can be checked from alpha to omega; you know what you have looked and haven't looked at, and when you're done. Sure, it has the usual combinatorial explosion of possible code paths making the task hard, but compared to a whole dimension of synthesized code, it looks like a walk in the park.
If you want to use currying to speed up operating system calls, get rid of the kernel/user boundary and have the whole system (application(s) plus kernel) in a functional language and have them running in one image. Then you can use actual currying (or closures, continuations). Those techniques don't require dynamic code synthesis.