Secure Application Development
Home faculty program location registration subscribe related past events	Elaborating security requirements by analysis of malicious anti-models In the modeling framework introduced by the first lecture, this lecture focuses on security goals and their obstacles. Techniques will be presented for elaborating security goals, for specifying them, and for analyzing them against conflicts and threats. Obstacles to security goals can be accidental or malicious. Malicious obstacles require hostile environments to be modeled in terms of attacker anti-goals, knowledge, and capabilities. In this setting, threat trees are built systematically through anti-goal refinement until leaf nodes are derived that are either software vulnerabilities observable by attackers or anti-requirements implementable by such attackers. New security requirements are then obtained as countermeasures through threat resolution operators. Such operators are applied to the specification of the anti-requirements and vulnerabilities revealed by the analysis. The optional formalization of security-critical parts of the system model provides additional benefits. Attacks can then be generated formally as anti-goal refinements; potential conflicts involving security goals can be detected formally; some of the countermeasure operators can be formalized to yield more precise countermeasures. The talk will introduce epistemic constructs and patterns for specifying various types of security goals in order to support the formal derivation of anti-goals, boundary conditions for conflict, and countermeasures.

Secure Application Development

Elaborating security requirements by analysis of malicious anti-models

In the modeling framework introduced by the first lecture, this lecture focuses on security goals and their obstacles. Techniques will be presented for elaborating security goals, for specifying them, and for analyzing them against conflicts and threats. Obstacles to security goals can be accidental or malicious. Malicious obstacles require hostile environments to be modeled in terms of attacker anti-goals, knowledge, and capabilities.

In this setting, threat trees are built systematically through anti-goal refinement until leaf nodes are derived that are either software vulnerabilities observable by attackers or anti-requirements implementable by such attackers. New security requirements are then obtained as countermeasures through threat resolution operators. Such operators are applied to the specification of the anti-requirements and vulnerabilities revealed by the analysis.

The optional formalization of security-critical parts of the system model provides additional benefits. Attacks can then be generated formally as anti-goal refinements; potential conflicts involving security goals can be detected formally; some of the countermeasure operators can be formalized to yield more precise countermeasures. The talk will introduce epistemic constructs and patterns for specifying various types of security goals in order to support the formal derivation of anti-goals, boundary conditions for conflict, and countermeasures.