Practical and Scalable Security Verification of Secure Architectures
This work addresses security verification for architects and developers, but appears incremental as it builds on existing verification concepts.
The paper tackles the problem of verifying security in secure architectures by proposing a framework that divides verification into external and internal components, and demonstrates its application on CloudMonatt and HyperWall architectures.
We present a new and practical framework for security verification of secure architectures. Specifically, we break the verification task into external verification and internal verification. External verification considers the external protocols, i.e. interactions between users, compute servers, network entities, etc. Meanwhile, internal verification considers the interactions between hardware and software components within each server. This verification framework is general-purpose and can be applied to a stand-alone server, or a large-scale distributed system. We evaluate our verification method on the CloudMonatt and HyperWall architectures as examples.