The Synthesis Kernel (1988) [pdf]
usenix.org
usenix.org
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.
My point is that although this paper doesn't discuss the security aspect, this work can be implemented in a secure manner.
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.
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.
Synthesis was one of my favorite papers - sort of more Unixy, traditional-ish than Self (another fav from that decade...)