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.
AVISPA @cite_32 is the tool for the automated validation of internet security protocols and applications. AVISPA provides a formal language for specifying security protocols and properties. It also integrates different back-ends that implement a variety of automatic analysis techniques. The four different back-ends are: OFMC (on-the-fly model checker), Sat-MC (SAT-based Model-Checker), TA4SP (Tree Automata based on Automatic Approximations for the Analysis of Security Protocols) and CL-AtSe (Constraint Logic based Attack Searcher). Protocols can be checked for security using two security goals: @math and @math which check that a value is not revealed to the attacker and that the remote party is authenticated, respectively.
@cite_32
2117064875
AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques. To the best of our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability.