A blog engine written and proven in Coq
coq-blog.clarus.me
A blog engine written and proven in Coq
1–10 of 60 posts
Re: A blog engine written and proven in Coq
#2> The purity of Coq ensures that each request is answered exactly once in finite time.
How does Coq ensure that the request completes in finite time?
Re: A blog engine written and proven in Coq
#3> The purity of Coq ensures that each request is answered exactly once in finite time. How does Coq ensure that the request completes in finite time?
At a guess it demonstrates that there's no possibility for infinite loops or recursion. It's going to rely on a model of the storage mechanism (memory, disk, whatever) that will respond to requests for data in finite time, but that doesn't seem an unreasonable assumption to make in this case. You have to draw the lines around your proof system somewhere or else you're going to end up having to model the entire world.
Re: A blog engine written and proven in Coq
#4This is great, as more real life examples are needed.
Re: A blog engine written and proven in Coq
#5The 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?
Re: A blog engine written and proven in Coq
#6The 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?
I 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.
Re: A blog engine written and proven in Coq
#7> The purity of Coq ensures that each request is answered exactly once in finite time. How does Coq ensure that the request completes in finite time?
Coq isn't Turing complete - it has a termination checker that needs to be able to determine that your functions terminate.
Re: A blog engine written and proven in Coq
#8The 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?
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.
Re: A blog engine written and proven in Coq
#9Is it also proven that no cross-site-scripting attacks are possible?
Re: A blog engine written and proven in Coq
#10> The purity of Coq ensures that each request is answered exactly once in finite time. How does Coq ensure that the request completes in finite time?
At a guess it demonstrates that there's no possibility for infinite loops or recursion. It's going to rely on a model of the storage mechanism (memory, disk, whatever) that will respond to requests for data in finite time, but that doesn't seem an unreasonable assumption to make in this case. You have to draw the lines around your proof system somewhere or else you're going to end up having to model the entire world.
> that doesn't seem an unreasonable assumption to make in this case
Not that I don't agree with you but I find it a common failure mode of HDs to just never reply to things. I guess it's also a common failure mode of network systems too.
Can Coq detect that you are enforcing I/O timeouts in a way that guarantees finite time?