freenode/#sicl - IRC Chatlog
Search
3:50:23
beach
jcowan: Why is that? Unix does not seem to need a machine-code verifier to make sure that user-level address spaces are always separate and that user code can't access kernel code.
4:16:04
beach
ACTION thinks that it's the word "trusted" that triggers people's reaction, and that he should invent another term for it.
4:17:40
beach
I mean, if we started saying that Unix is of type "trusted C compiler and trusted programmer to never use any undefined behavior in C", perhaps the difference between Unix and what I am trying to do would me clearer.
8:14:35
beach
jcowan: I do want to thank you for pointing out the importance of terminology. I change the terminology in the document from "trusted compiler" to "controlled access system" and plan to use the term "arbitrary access system" for the traditional technology.
8:33:18
jcowan
beach: Unix and other OSes do indeed have a machine code verifier of that type, but rather than being an AOT abstract interpreter, it's a JIT verifier that is part of the hardware's concrete interpreter.
8:35:23
beach
If it's part of the hardware, I don't see how the compiler (say GCC) can be trusted. Nor do I see how the programmer can be trusted not to use undefined behavior. In fact, I am pretty sure that a lot of C code used to write kernels exploits undefined behavior that happens to work with the compiler in question.
8:51:20
jcowan
That is merely as much as to say that nothing created by mortals can be trusted absolutely.
8:52:16
beach
Because if I use that terminology, the immediate reaction of many readers is to try to hold me to higher standards than they would other systems.
8:53:07
jcowan
What I am saying, terminology aside, is that it should be possible to write a verifier in which one may repose more confidence than in the compiler as a whole, which has many duties, and that by doing so the overall security/reliability of the system is improved.
8:54:52
beach
For me, it is enough to imagine the mechanism that I think will give much higher safety than current systems can provide.
8:55:07
heisig
Yes, I think the point is not about trust, but that the probability of getting a safe system is much higher if safety is provided by the compiler and the runtime.
8:55:34
jcowan
Well, I am intimately familiar with what working with a system that doesn't use hardware memory protection is like, and it's much like riding a unicycle, even when assembly language programming is avoided.
8:58:17
beach
Then I think they are quite incomparable to the suggested CLOSOS system which will use only Common Lisp.
8:59:24
jcowan
heisig: I find it hard to believe that using software protection only (i.e. safety by construction) is safer than using hardware isolation.
9:01:40
beach
With a system that allows a process full access to its address space, you get all the problems with accessing the stack, having shared libraries in the same space, etc.
9:02:23
beach
It is that the typical hardware solution exposes so many security problems that require each application to be written in a very careful way in order to be safe.
9:02:49
beach
So with the hardware solution, there are way more points of failure (every application program).
9:04:23
heisig
jcowan: The problem of hardware isolation is that it works at a very low level. It only ensures some very basic properties, such as memory safety. It does not ensure that you have a consistent CL runtime.
9:06:09
heisig
The point of SICL is that no matter how bad a programmer screws up, there will still be a REPL and some restarts for him. I thank that is extraordinarily more useful than what we have today.
9:18:11
heisig
beach: Don't! Or, do both. But I definitely know this feeling. Whenever I use a computer I envy my grandfather who used to be a stove setter.
9:19:26
beach
I am joking, of course. After decades of working with software, I can no longer handle domains that require repeated work just to keep the status quo.
9:20:34
Shinmera
beach: repeated work only to keep the status quo sounds like a lot of what's happening in software too though
9:29:59
jcowan
Well, all readers (certainly including me) read new things through the lens of all they have read before, and undoubtedly I have not read carefully enough.
9:30:30
jcowan
However, I should make clear that by a verifier I do not mean something that does formal verification of correctness, a notion in which I do not believe.
9:32:35
jcowan
Rather, I wish you to address the skeptical reader who says, "I agree that there are problems around sharing (intentional and unintentional) with the present hardware-assisted separation mechanism, but you would have me believe that your compiler will not produce code that behaves like uncontrolled assembly-language code.
9:33:19
jcowan
If there were a component simpler than the whole compiler which would provide further assurance that its output is safe in some sense, that would raise my confidence level considerably."
9:35:21
beach
I am thinking that an ordinary Common Lisp compiler that does not exploit undefined behavior is safe. I can't think of any interactions with the REPL that I would be able to do that would generate some arbitrary machine code to access any address in memory.
9:36:24
beach
By "ordinary Common Lisp compiler", I mean what the standard allows me to type, as opposed to accessing the guts of the compiler to modify it and then use the modified compiler.
9:37:01
no-defun-allowed
the most dangerous one i can think of would be dynamic-extent but you could likely ignore that since a good gc is as fast as the stack for most of the time
9:37:21
jcowan
Just as a simple example, a verifier might verify that there are no branches in a compiled method that extend beyond the boundaries of the method.
9:37:33
beach
no-defun-allowed: I am determined to ignore it unless the compiler can prove that it's safe to exploit it.
9:38:34
jcowan
Or that the target of a branch is in all cases the start of an instruction, given that instructions may be multiple bytes long.
9:39:51
jcowan
Abstract interpretation can verify the absence of overflows or underflows in the stack frame.
9:41:27
jcowan
The point is that my confidence in the correctness of these checks is much greater than my confidence in the correctness of compiled output, in the same way that tests can strengthen one's confidence in the correctness of code.
9:44:01
beach
jcowan: I intend to write the compiler in such a way that both of those properties are true. I have no ambition to write a separate verifier for that. It is my experience that defects like that would be detected very quickly because some spectacular failure would happen. If someone else feels like writing such a verifier that's great.
9:47:28
jcowan
Fair enough. I certainly didn't mean to say that you should do it, simply that I believe it is a requirement for a shared-space single-compiler system to be accepted as safe enough to be usable.
9:48:31
jcowan
Note also that in an infinitely pliable system the compiler is as open to change as anything else (perhaps there are special protections for it, I don't know)
9:49:07
beach
jcowan: My job is to do research in computer science. The entire purpose of the CLOSOS project is to demonstrate that we can do better than we currently do in terms of safety and security, or rather, to convince enough smart people that this concept will make it possible to do better. I will very likely not be able to accomplish a completely finished system by myself. Maybe a finished system will never happen, and that's fine too.
9:53:26
beach
The code of the compiler will live in a first-class global environment that is not usually accessible to the ordinary user. Just like installing kernel modules in a Unix-like system requires some admin privileges, modifying the compiler will also require such privileges.
9:54:30
beach
The point is not to prevent a hacker from improving the compiler, but to prevent malicious code to do harm when the user is only doing ordinary day-to-day tasks (i.e. not hacking the compiler).
10:06:43
jcowan
Well, I would simply urge you to consider adding a paragraph to chapter 3 that presents the possibility of a post-compilation, pre-execution abstract interpreter of compiled functions that provides further assurance that the compiler's output is not deranged.
10:07:23
jcowan
This will be a very familiar idea to (a) computer scientists familiar with abstract interpretation, which is some 40 years old by now and (b) programmers who are accustomed to having their compiled programs verified (in this limited sense) by the various VMs on which they run.
10:09:02
beach
Thanks for the advice. I won't be doing that right now, because I have more urgent tasks, like ELS papers, SICL bootstrapping, and such. But I'll put it on my list of things to do.
10:13:37
jcowan
I'll just add that another advantage of the abstract interpreter is that, since it is probably simpler than any compiler, it permits machine-code compilers (as opposed to translators-to-CL) for various languages to exist on CLOSOS in parallel with the CL compiler.
10:13:44
jcowan
There is nothing inherently impossible about a safe compiler for strictly conforming C, though it cannot be as efficient as a safe compiler for more tractable languages.
10:18:52
no-defun-allowed
jcowan: I know the feels. Sleep to some extent that makes you less tired :)