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
cryptography@metzdowd.com
http://www.metzdowd.com/mailman/listinfo/cryptography
