On the derivation of secure components

摘要

The author discusses the problems in deriving a system from itsnspecification when that specification includes simple trace-basedninformation-flow security properties as well as safety properties. Henpresents two fundamental theorems of information-flow security whichndescribe the inherent difficulties of deriving secure implementationsnand considers the implications of these results. It is concluded that itnis dangerous to extrapolate from success in the case of two to the casenof many. Results proved about systems with just low- and high-accessnusers may not extend easily to full lattices