The Synthesis Kernel (1988) [pdf](usenix.org)
usenix.org
The Synthesis Kernel (1988) [pdf]
https://www.usenix.org/legacy/publications/compsystems/1988/win_pu.pdf
6 comments
This 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.
This could apply as a partial general explanation: https://news.ycombinator.com/item?id=15048914
It 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.
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.
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.
[0] http://dl.acm.org/citation.cfm?id=2661142
My point is that although this paper doesn't discuss the security aspect, this work can be implemented in a secure manner.
[0] http://dl.acm.org/citation.cfm?id=2661142
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.
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.
You can just get it off Libgen as usual: http://dl.acm.org.sci-hub.io/citation.cfm?id=2661142
Man that strikes close to home! Breaking invariants when nobody observes it.
I did something in this spirit in my Lisp dialect.
I broke the invariant which says "no matter how you terminate a form, the unwind-protect cleanup forms get called".
I broke it by introducing the concept of "absconding": leaving a scope in such a way that the local resources tied to lexical/dynamic contours are left alone. No unwinding calls are done.
The justification is precisely that it is OK if the scope is later re-entered (specifically: restarted via revived continuation). The revived control then finds everything intact --- and can leave the scopes normally at which point the cleanup does take place.
By doing this, I solved the problem of how to integrate continuations with scoped resource acquisition/cleanup, without the horror of dynamic-wind or its ilk.
I did something in this spirit in my Lisp dialect.
I broke the invariant which says "no matter how you terminate a form, the unwind-protect cleanup forms get called".
I broke it by introducing the concept of "absconding": leaving a scope in such a way that the local resources tied to lexical/dynamic contours are left alone. No unwinding calls are done.
The justification is precisely that it is OK if the scope is later re-entered (specifically: restarted via revived continuation). The revived control then finds everything intact --- and can leave the scopes normally at which point the cleanup does take place.
By doing this, I solved the problem of how to integrate continuations with scoped resource acquisition/cleanup, without the horror of dynamic-wind or its ilk.
apparently Massalin is still at MicroUnity after 20 years. does anyone know if they do any business outside of patent licensing?
Mods: This needs a (1988)
ow! 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...)
Synthesis was one of my favorite papers - sort of more Unixy, traditional-ish than Self (another fav from that decade...)