Model Checking and Security
Model checking is a technique of verifying temporal properties of finite-state systems. One of
the attractive features of model checking over other techniques (such as theorem proving)
is that if a property is not true, a model checker provides a counter-example which
explains why the property is not true. Inventors of model checking, Edmund Clarke,
Allen Emerson, and Joseph Sifakis, won the 2008 ACM Turing award (see the announcement here). I have a personal connection to two of the recipients. Edmund Clarke was my adviser
at Carnegie Mellon, and Allen Emerson and I have collaborated on few projects and he
has supported me through out my career.
In this note I try to summarize various applications of model checking to security.
Protocol verification: Protocols in the realm of security (henceforth referred to
as security protocols) are very tricky to get correct. For
example, flaws in authentication protocols have been discovered several years after they have been published. Techniques based on model checking have been extensively used to verify these protocols. The tricky part in applying these techniques for verifying security protocols is
modeling the capabilities of the attacker. Gavin Lowe used the FDR model checker to find
a subtle attack on the Needham-Schroeder authentication protocol (this
publication can found here). Following Lowe's work there
was a flurry of activity on this topic. Interested readers can look at the proceedings of
the Computer Security Foundations Symposium (CSF).
Vulnerability assessment: Imagine you are given an enterprise network with various components (firewalls, routers, and Intrusion Prevention Systems (IPSs)).
Vulnerability assessment tries to ascertain how an attacker can penetrate the specified network. Vulnerability assesment is crucial in updating policies of various security appliances (such as firewalls and IPSs) and ascertaining the risk of various decisions. Traditionally, vulnerability assessment has been performed by red teams. Red teaming is a very valuable activity but can provide no guarantees that the entire state space of vulnerabilities has been explored. I along with (Oleg Sheyner and Jeannette Wing) explored techniques based on model checking for vulnerability assessment. We formally specify the network and express the negation of the attackers goal (e.g., attacker gets root access on a critical server) as a property to be verified. If
the specified network is vulnerable, then the model checker will output a counter-example (which is an attack on the network). The innovation we devised was to output the set of all
counter-examples or attacks as an attack graph, which is succinct representation of all attacks on the network. Analysis of the attack graph can provide a basis for vulnerability assessment. This paper can be downloaded here.
Other applications: There are several problems in security that can be addressed using model checking. For example, I and Tom Reps have used model checking properties to analyze properties of security policies in trust-management systems. Ninghui Li and his collaborators have used techniques based on model checking to analyze several classes of security properties.
In the context of security, the advantage model checking has over other techniques (such as
testing) is that it exhaustively covers the state-space. After all, if you just have one
vulnerability, an attacker will exploit that vulnerability, i.e., an attacker just needs one
door to get through your system. Thus the completeness guarantee that a model checker provides is very valuable in the context of security.
the attractive features of model checking over other techniques (such as theorem proving)
is that if a property is not true, a model checker provides a counter-example which
explains why the property is not true. Inventors of model checking, Edmund Clarke,
Allen Emerson, and Joseph Sifakis, won the 2008 ACM Turing award (see the announcement here). I have a personal connection to two of the recipients. Edmund Clarke was my adviser
at Carnegie Mellon, and Allen Emerson and I have collaborated on few projects and he
has supported me through out my career.
In this note I try to summarize various applications of model checking to security.
Protocol verification: Protocols in the realm of security (henceforth referred to
as security protocols) are very tricky to get correct. For
example, flaws in authentication protocols have been discovered several years after they have been published. Techniques based on model checking have been extensively used to verify these protocols. The tricky part in applying these techniques for verifying security protocols is
modeling the capabilities of the attacker. Gavin Lowe used the FDR model checker to find
a subtle attack on the Needham-Schroeder authentication protocol (this
publication can found here). Following Lowe's work there
was a flurry of activity on this topic. Interested readers can look at the proceedings of
the Computer Security Foundations Symposium (CSF).
Vulnerability assessment: Imagine you are given an enterprise network with various components (firewalls, routers, and Intrusion Prevention Systems (IPSs)).
Vulnerability assessment tries to ascertain how an attacker can penetrate the specified network. Vulnerability assesment is crucial in updating policies of various security appliances (such as firewalls and IPSs) and ascertaining the risk of various decisions. Traditionally, vulnerability assessment has been performed by red teams. Red teaming is a very valuable activity but can provide no guarantees that the entire state space of vulnerabilities has been explored. I along with (Oleg Sheyner and Jeannette Wing) explored techniques based on model checking for vulnerability assessment. We formally specify the network and express the negation of the attackers goal (e.g., attacker gets root access on a critical server) as a property to be verified. If
the specified network is vulnerable, then the model checker will output a counter-example (which is an attack on the network). The innovation we devised was to output the set of all
counter-examples or attacks as an attack graph, which is succinct representation of all attacks on the network. Analysis of the attack graph can provide a basis for vulnerability assessment. This paper can be downloaded here.
Other applications: There are several problems in security that can be addressed using model checking. For example, I and Tom Reps have used model checking properties to analyze properties of security policies in trust-management systems. Ninghui Li and his collaborators have used techniques based on model checking to analyze several classes of security properties.
In the context of security, the advantage model checking has over other techniques (such as
testing) is that it exhaustively covers the state-space. After all, if you just have one
vulnerability, an attacker will exploit that vulnerability, i.e., an attacker just needs one
door to get through your system. Thus the completeness guarantee that a model checker provides is very valuable in the context of security.
Comments
Network Security Models With Examples