archives

Delegating Responsibility in Digital Systems: Horton's "Who Done It?"

Jed Donnelley, Alan Karp, and I would like your comments on our draft paper

Delegating Responsibility in Digital Systems:
Horton's "Who Done It?"

Programs do good things, but also do bad,
making software security more than a fad.
The authority of programs, we do need to tame.
But bad things still happen. Who do we blame?

From the very beginnings of access control:
Should we be safe by construction,
or should we patrol?
Horton shows how, in an elegant way,
we can simply do both, and so save the day.

with apologies to Dr. Seuss

We plan to submit it to USENIX HotSec 07 (Hot Topics in Security) which has a five page limit. Submission deadline is 6/1/2007. We think this paper is important. Your comments and suggestions will be greatly appreciated. Thanks!

Social Processes and Proofs of Theorems and Programs

A paper that was mentioned in the discussion forum, by Richard A. De Millo, Richard J. Lipton, Alan J. Perlis, 1979.
It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore, the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real progarms make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language deisgn.