Security check: a formal yet practical framework for secure software architecture

With security becoming an important concern for both users as well as designers of large-scale software systems, it is necessary to introduce security considerations very early in the system development life-cycle namely in the modeling phase itself. But the main problem in the widespread adoption of security modeling has been that representations of even moderate-size systems consume so much memory (due to the infamous state space explosion problem) that designers are loathe to spend time increasing the complexity of their models by introducing security aspects in the design phase itself. In this paper we propose a technique called security check which entails taking small units of a system, putting them in a "security harness" that exercises relevant executions appropriately within the unit, and then model checking these more tractable units. For most systems whose security requirements are localized to individual system components or interactions between small numbers of components, security check offers a means of coping with state explosion. Another major benefit of security check is that it enables us to detect system vulnerabilities even when the attack behavior is not known. And for known attack patterns security check can provide models of suspicious behavior which can then be used for intrusion detection at a later stage.