[langsec-discuss] Is computation half the story?
sbg at acw.com
Fri Mar 27 13:10:35 UTC 2015
>>> By "theory" I mean a general system of knowledge and understanding.
>>> Think "theory of evolution", not "theorems."
But why not think theorems? A general theory while certainly helpful for
framing questions can not be the foundation for making security assertions
about a system at hand any more than the general theory of evolution tells
us how the eye evolved. The theorem approach has worked well in the area
of authentication protocols and has led to the discovery of undesirable
propertie. The break of the Needham and Schroeder protocol is, perhaps, the
most well-known example. Nobody knew the hole was there until Gavin Lowe
among others tried to prove the a property of the protocol that wasn't
Formal analysis (the theorem approach) can handle composition of systems and
cascading of systems in the same manner that today's mathematics is built on
yesterday's. Boyer and Moore proved theorems about an entire computational
stack from chip net list to programming language.
Yes, it's hard work. But it yields hard results. General theories are
necessary for the framework but they can't tell us anything specific such as
can Attack A succeed against System B. People running and using
computational systems need specifics, not generalities.
IMHO, as always.
More information about the langsec-discuss