[Cryptography] The Case for Formal Verification

[Jerry Leichter]

On Aug 29, 2013, at 7:00 PM, Phillip Hallam-Baker wrote:
> ...The code synthesis scheme I developed was an attempt to address the scaling problem from the other end. The idea being that to build a large system you create a very specific programming language that is targeted at precisely that class of problems. Then you write a back end that converts the specification into code for that very restricted domain. If you want a formal proof you have the synthesizer generate it from the specification as well. That approach finesses the problem of having to validate the synthesizer (which would likely take category theory) because only the final target code need be validated....
Many years back, I did some work with Naftaly Minsky at Rutgers on his idea of "law-governed systems".  The idea was that you have an operational system that is wrapped within a "law enforcement" system, such that all operations relevant to the "law" have to go through the enforcer.  Then you write "the law" to specify certain global properties that the implementation must always exhibit, and leave the implementation to do what it likes, knowing that the enforcer will force it to remain within the law.

You can look at this in various ways in modern terms:  As a generalized security kernel, or as the reification of the attack surface of the system.

Minsky's interests were more on the software engineering side, and he and a couple of grad students eventually put together a law-governed software development environment, which could control such things as how modules were allowed to be coupled.  (The work we did together was on an attempt to add a notion of obligations to the law, so that you could not just forbid certain actions, but also require others - e.g., if you receive message M, you must within t seconds send a response; otherwise the law enforcer will send one for you.  I'm not sure where that went after I left Rutgers.)

While we thought this kind of thing would be useful for specifying and proving security properties, we never looked at formal proofs.  (The law of the system was specified in Prolog.  We stuck to a simple subset of the language, which could probably have been handled easily by a prover.  Still, hardly transparent to most programmers!)
                                                        -- Jerry