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

The cryptography mailing list

Reply via email to