| This is a bit off-topic, but hopefully interesting. | | Rather than trying to prove a program to be correct (which I agree is doomed | to failure for the forseeable future for all but trivial programs), perhaps | it would be useful to have an automated therom-prover to try to deduce | "interesting things" about certain programs such as "this program always | bounds-checks its input", "this program allows writes to arbitrary files on | lines x, y, and z", "this program halts". (:>) I'm doing a PhD on runtime information flow analysis of programs, tracking each datum and who has contributed to it. Each datum has an associated set of subjects that has contributed, and each system call checks whether all subjects in the set are granted the call or not. This tracking is done by compiled-in 'shadowing' code, compiled in into the binary, and the code is inserted based on something similar to 'data flow' analysis. Its messy, but I think it might work out in the end. This kind of access control is much better suited for extensive communication between different subjects than the current paradigm of having an owner of the process. With the current concept, it is imperative for the process to filter and controll each datum entering the process, since it might be 'hostile'. (The current concept of identity is really based on *partitioning* an expensive computing facility, without communication between the different partitions.) I believe this task to be to burdening in the long run. With "my approach", you can accept any input without fear, since it will be stopped when your application does the syscall. I just started, so I don't have anything concrete yet. I'll have it in five years! :-) | Obviously (as the last example illustrates), this isn't perfect because | something can be true without being provable. Why ever prove anything else but a trace of actual execution? This is usually almost trivial, you don't have the problem of calculating the proof for all possible branches, etc... | Further, it's likely that assumptions must be made about system calls, | libraries, and the ways in which they interact. It might be fruitful to do it for an actual system, although I think that this "paradigm"-shift will influence a lot of the design of the system. | However, I think such a tool would be useful because | it may quickly point out things not obvious to (most) humans | and getting some idea of what can't be deduced and why would be instructive. Tell me if your planning to do something along these lines, it would be most interesting. Regards, Christian