3 ms·
The last line threw me off: > an unauthenticated user cannot access private pages (like edit) or modify the file system with system calls. System calls? How d
by hrjet 12y ago
The last line threw me off:
> an unauthenticated user cannot access private pages (like edit) or modify the file system with system calls.
System calls? How do they come into the picture? And wouldn't reasoning about system calls require proofs about the kernel itself?
- vog 12y agoI guess this merely means that it is proven that no such system calls are executed directly. Of course, in theory there might be some kernel bug such that e.g. a read() sometimes changes files on disk, but I guess this is outside the scope of that proof system. Only the blog program itself was proven, assuming that the remaining system software as well as hardware are working in a sane way. If you want your proofs to include the whole operating system, you'd first have to reduce the kernel to a minimal operating system (e.g. MirageOS). If have lots of time, money and motivation, you could continue to include the possibly used virtualization layer (XEN, QEMU/KVM, whatever) and finally the hardware design.
- kriro 12y agoWithout reading the sourcecode/proof (bookmarked for later) my guess is that it simply means something along the lines of "the user cannot execute code a la eval". So basically the user can do exactly the specified actions and nothing more.
- clarus 12y agoBy "system call", we do not mean "kernel call" but more "call to the system" in a broader sense, that is from the program to its environment (it could be the OS or other libraries). We should probably use another word since this is confusing. More exactly, we check that the only calls when the user is not logged in are: ReadFile, ListPosts or Log: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#l208 https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#...