On Tue, 1 Aug 1995, Dr. Frederick B. Cohen was alleged to have blathered:
Tim May mused:
Anything that "reaches out" to external libraries or utilities would then have the vulnerabilities of _those_ libraries and utilities, which may or may not be provably correct themselves. (And the issue of any PRNG being probably correct or not is of course an interesting, and deep, question.)
I do think the issues of modular design and provable correctness--or approximations to it--are interesting ones.
I think that this issue can generally be addressed by a divide and conquer strategy. Prove that the called routines are correct and confined under all possible parameters, do the same for the calling routines, do the same for the interaction between them, and I think you have it. This is pretty easy for one or two routines, but when you take the OS into account, the C compiler into account, the program itself into account, and the external environment into account, you run into some serious limitations. For example, you may (in some cases) have to show that under all possible sequences of interrupt timings and stack conditions, the system operates correctly (which almost none currently do). Unless you design with this sort of thing in mind, it's very hard to demonstrate these properties even for limited subproblems.
After all your griping over PGP, you spout this? Have you ever heard of Godel's theorem? I have a phrase for people who peddle their mark of approval that a given large program will work: "Snake oil salesman". In the messages which you have scrawled between this and the last on my system when I caught up this evening, you have demonstrated the fraudulent nature of your business by first claiming that certain propositions were "demonstrated", then stating that a graduate student was working on "proving" them. I repeat: Snake Oil Salesman <PLONK>