3 ms·
Without 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 eva
by kriro 12y ago
Without 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#...