|
What are the Right Roles for Formal Methods in
High Assurance Cloud Computing?
Ken Birman (Cornell University)
The developer of a high assurance system must
justify the fitness of the system for the intended use. In "small"
scenarios, this problem is well understood: it entails rigorously
specifying properties the system must achieve, designing protocols and
correctness proofs, and then implementing and testing the needed code.
In scaled-out settings, complex architectures are often unavoidable and
this methodology can no longer be used. I'll suggest that high assurance
for large, complex systems can (only) be tackled successfully using an
approach similar to aspect oriented programming, with different
assurance concerns approached in very different ways.
[Slides] |
