Wednesday, March 19, 2008

Botnets in USA Today

I got a call from Byron Acohido over at the USA Today last weekend,
and we had an interesting talk about botnets. Byron and Jon Swartz ended
up writing an article about botnets which appeared as the cover story
in the Money section of the USA Today on March 17, 2008. Here's a link to the full
story (link). I found the entire article to be a fascinating read
on the nature of botnets. Here are some of the highlights, but
definitely go and read the entire article.
  • On a typical day, 40% of the 800 million computers connected to the Internet are bots engaged in various nefarious activities, such as spamming, stealing sensitive data, and engaging in denial-of-service attacks. Think about it. Approximately 320 million computers are engaged these illicit actiivities!
  • Later on in the article they describe various features of Storm, the state-of-the-art for botnets. Storm introduced various innovations into the bot landscape, such as using P2P style communication to converse with the bots and encrypting the command-and-control (C&C) traffic. Command-and-control is the traffic from the bot-herder to the bots instructing them to perform various nefarious activities. Note that this means that various network-based botnet solutions that simply look for centralized C&C communication will not work. Moreover, encrypted traffic is a major problem for the network-based solutions. See my earlier blog where I argue that we should move to a cooperative solution. This is looking like a very good idea. Storm also has a self-defense mechanism, i.e., anyone trying to probe the botnet is punished with a denial-of-service attack. I found this self-defense mechanism of Storm to be very interesting.
Overall a fascinating article!
I plan to drop by Byron's book signing at the RSA Conference in San
Francisco on April 7th. Byron also has an interesting blog which is related to the
material in the book.

Wednesday, March 5, 2008

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.