|
Security '05 Paper   
[Security '05 Technical Program]
MulVAL: A Logic-based Network Security Analyzer * Xinming Ou Sudhakar Govindavajhala Andrew W. Appel
Abstract:To determine the security impact software vulnerabilities have on a particular network, one must consider interactions among multiple network elements. For a vulnerability analysis tool to be useful in practice, two features are crucial. First, the model used in the analysis must be able to automatically integrate formal vulnerability specifications from the bug-reporting community. Second, the analysis must be able to scale to networks with thousands of machines. We show how to achieve these two goals by presenting MulVAL, an end-to-end framework and reasoning system that conducts multihost, multistage vulnerability analysis on a network. MulVAL adopts Datalog as the modeling language for the elements in the analysis (bug specification, configuration description, reasoning rules, operating-system permission and privilege model, etc.). We easily leverage existing vulnerability-database and scanning tools by expressing their output in Datalog and feeding it to our MulVAL reasoning engine. Once the information is collected, the analysis can be performed in seconds for networks with thousands of machines. We implemented our framework on the Red Hat Linux platform. Our framework can reason about 84% of the Red Hat bugs reported in OVAL, a formal vulnerability definition language. We tested our tool on a real network with hundreds of users. The tool detected a policy violation caused by software vulnerabilities and the system administrators took remediation measures.
|
Platform | Submitted | Accepted |
Microsoft Windows | 543 | 489 |
Red Hat Linux | 203 | 202 |
Sun Solaris | 73 | 57 |
Total | 819 | 748 |
For example, we ran the OVAL scanner on one
machine using the latest OVAL definition file and
found the following vulnerabilities:
VULNERABILITIES FOUND: OVAL Id CVE Id ------------------------- OVAL2819 CAN-2004-0427 OVAL2915 CAN-2004-0554 OVAL2961 CAN-2004-0495 OVAL3657 CVE-2002-1363 -------------------------
We convert the output of an OVAL scanner into Datalog clauses like the following:
vulExists(webServer, 'CVE-2002-0392', httpd).
Besides producing a list of discovered vulnerabilities, the OVAL scanner can also output a detailed machine configuration information in the System Characteristics Schema. Some of this information is useful for reasoning about multistage attacks. For example, the protocol and port number a service program is listening on, in combination with the firewall rules and network topology expressed as HACL, helps determine whether an attacker can send a malicious packet to a vulnerable program. Currently the following predicates about machine configurations are used in the reasoning engine.
networkService(Host, Program, Protocol, Port, Priv). clientProgram(Host, Program, Priv). setuidProgram(Host, Program, Owner). filePath(H, Owner, Path). nfsExport(Server, Path, Access, Client). nfsMountTable(Client, ClientPath, Server, ServerPath).
networkService describes the port number and protocol under which a service program is listening and the user privilege the program has on the machine. If the same server is listening under multiple ports and protocols, this is described by multiple networkService statements. clientProgram describes the privilege of a client program once it gets executed. setuidProgram specifies an a setuid executable on the system and its owner. filePath specifies the owner of a particular path in the file system. nfsExport describes which portion of the file system on an NFS server is exported to a client. nfsMountTable describes an NFS mounting table entry on the client machine. The scanner used in MulVAL is implemented by augmenting a standard off-the-shelf OVAL scanner, such that it not only reports the existence of vulnerabilities, but also outputs machine configuration information in the form of these predicates.
One can find detailed information about the vulnerabilities from OVAL's web site.2 For example, the OVAL description for the bug OVAL2961 is:
Multiple unknown vulnerabilities in Linux kernel 2.4 and 2.6 allow local users to gain privileges or access kernel memory, ...
This informal short description highlights the effect of the vulnerability -- how the vulnerability can be exploited and the consequence it can cause. If a machine-readable database were to provide information on the effect of a bug such as bug 2961 is only locally exploitable, one could formally prove properties like if all local users are trusted, then the network is safe from remote attacker. Unfortunately, OVAL does not present the information about the effect of a vulnerability in a machine readable format. Fortunately, the ICAT database [18] classifies the effect of a vulnerability in two dimensions: exploitable range and consequences.
A local exploit requires that the attacker already have some local access on the host. A remote exploit does not have this requirement. Two most common exploit consequences are privilege escalation and denial of service. Currently all OVAL definitions have corresponding ICAT entries (the two can be cross-referenced by CVE Id). It would be nice if OVAL and ICAT be merged into a single database that provides both information.
We converted the above classification in the ICAT database into Datalog clauses such as
vulProperty('CVE-2004-00495', localExploit, privEscalation).
The reasoning rules in MulVAL are declared as Datalog clauses. A literal, p(t1,..., tk) , is a predicate applied to its arguments, each of which is either a constant or a variable. In the formalism of Datalog, a variable is an identifier that starts with an upper-case letter. A constant is one that starts with a lower-case letter. Let L0, ..., Ln be literals, a sentence in MulVAL is represented as a Horn clause:
L0 :- L1, ..., Ln
Semantically, it means if L1, ..., Ln are true then L0 is also true. The left-hand side is called the head and the right-hand side is called the body. A clause with an empty body is called a fact. A clause with a nonempty body is called a rule.
MulVAL reasoning rules specify semantics of different kinds of exploits, compromise propagation, and multihop network access. Currently there are 24 rules in MulVAL. The MulVAL rules are carefully designed so that information about specific vulnerabilities are factored out into the data generated from OVAL and ICAT. The interaction rules characterize general attack methodologies (such as ``Trojan Horse client program''), not specific vulnerabilities. Thus the rules do not need to be changed frequently, even if new vulnerabilities are reported frequently.
We introduce several predicates that are used in the exploit rules. execCode(P,H,UserPriv) indicates that principal P can execute arbitrary code with privilege UserPriv on machine H. netAccess(P, H, Protocol, Port) indicates principal P can send packets to Port on machine H through Protocol.
The effect classification of a vulnerability indicates how it can be exploited and what is the consequence. We have already seen a rule for remote exploit of a service program in section 2. Following is the exploit rule for remote exploit of a client program.
execCode(Attacker, Host, Priv) :- vulExists(Host, VulID, Program), vulProperty(VulID, remoteExploit, privEscalation), clientProgram(Host, Program, Priv), malicious(Attacker).
The body of the rule specifies that 1) the Program is vulnerable to a remote exploit; 2) the Program is client software with privilege Priv;3 3) the Attacker is some principal that originates from a part of the network where malicious users may exist. The consequence of the exploit is that the attacker can execute arbitrary code with privilege Priv.
The rule for the exploit of a local privilege escalation vulnerability is as follows:
execCode(Attacker, Host, Owner) :- vulExists(Host, VulID, Prog), vulProperty(VulID, localExploit, privEscalation), setuidProgram(Host, Prog, Owner), execCode(Attacker, Host, SomePriv), malicious(Attacker).
For this exploit, the precondition execCode requires that an attacker first have some access to the machine Host. The consequence of the exploit is that the attacker can gain privilege of the owner of a setuid program.
In our model, the Linux kernel is both a network service running as root, and a setuid program owned by root. That is, the consequence of exploiting a privilege-escalation bug in kernel (either local or remote) will result in a root compromise.
Currently we do not have exploit rules for vulnerabilities whose exploit consequence is confidentiality loss or integrity loss. The ICAT database does not provide precise information as to what confidential information may be leaked to an attacker and what information on the system may be modified by an attacker. ICAT statistics shows that 84% of vulnerabilities are labeled with privilege-escalation or only labeled with denial-of-service, the two kinds of exploits modeled in MulVAL. It seems in reality privilege-escalation bugs are the most common target for exploit in a multistage attack.
For example, the following rule says if an attacker P can access machine H with Owner's privilege, then he can have arbitrary access to files owned by Owner.
accessFile(P, H, Access, Path) :- execCode(P, H, Owner), filePath(H, Owner, Path).
On the other hand, if an attacker can modify files under Owner's directory, he can gain privilege of Owner. That is because a Trojan horse can be injected by modified execution binaries, which Owner might then execute:
execCode(Attacker, H, Owner) :- accessFile(Attacker, H, write, Path), filePath(H, Owner, Path), malicious(Attacker).
accessFile(P, Server, Access, Path) :- malicious(P), execCode(P, Client, root), nfsExportInfo(Server, Path, Access, Client), hacl(Client, Server, rpc, 100003)),
hacl(Client, Server, rpc, 100003) is an entry in host access control list (section 4.2), which specifies machine Client can talk to Server through NFS, an RPC (remote procedure call) protocol with number 100003.
netAccess(P, H2, Protocol, Port) :- execCode(P, H1, Priv), hacl(H1, H2, Protocol, Port).
If a principal P has access to machine H1 under some privilege and the network allows H1 to access H2 through Protocol and Port, then the principal can access host H2 through the protocol and port. This allows for reasoning about multihost attacks, where an attacker first gains access on one machine inside a network and launches an attack from there. Predicate hacl stands for an entry in the host access control list (HACL).
hacl(Source, Destination, Protocol, DestPort).
Packet flow is controlled by firewalls, routers, switches, and other aspects of network topology. HACL is an abstraction of the effects of the configuration of these elements. In dynamic environments involving the use of Dynamic Host Configuration Protocol (especially in wireless networks), firewall rules can be very complex and can be affected by the status of the network, the ability of users to authenticate to a central authentication server, etc. In such environments, it is infeasible to ask the system administrator to manually provide all HACL rules. We envision that an automatic tool such as the Smart Firewall [4] can provide the HACL list automatically for our analysis.
The security policy specifies which principal can access what data. Each principal and data is given a symbolic name, which is mapped to a concrete entity by the binding information discussed in section 4.4. Each policy statement is of the form
allow(Principal, Access, Data).
The arguments can be either constants or variables (variables start with a capital letter and can match any constant). Following is an example policy:
allow(Everyone, read, webPages). allow(user, Access, projectPlan). allow(sysAdmin, Access, Data).
The policy says anybody can read webPages, user can have arbitrary access to projectPlan. And sysAdmin can have arbitrary access to arbitrary data. Anything not explicitly allowed is prohibited.
The policy language presented in this section is quite simple and easy to make right. However, the MulVAL reasoning system can handle more complex policies as well (see section 4.6).
Principal binding maps a principal symbol to its user accounts on network hosts. For example:
hasAccount(user, projectPC, userAccount). hasAccount(sysAdmin, webServer, root).
Data binding maps a data symbol to a path on a machine. For example:
dataBind(projectPlan,workstation,'/home'). dataBind(webPages, webServer, '/www').
The binding information is provided manually.
The analysis algorithm is divided into two phases: attack simulation and policy checking. In the attack simulation phase, all possible data accesses that can result from multistage, multihost attacks are derived. This is achieved by the following Datalog program.
access(P, Access, Data) :- dataBind(Data, H, Path), accessFile(P, H, Access, Path).
That is, if Data is stored on machine H under path Path, and principal P can access files under the path, then P can access Data. The attack simulation happens in the derivation of accessFile, which involves the Datalog interaction rules and data tuple inputs from various components of MulVAL. For a Datalog program, there are at most polynomial number of facts that can be derived. Since XSB's tabling mechanism guarantees each fact is computed only once, the attack simulation phase is polynomial.
In the policy checking phase, the data access tuples output from the attack simulation phase are compared with the given security policy. If an access is not allowed by the policy, a violation is detected. The following Prolog program performs policy checking.
policyViolation(P, Access, Data) :- access(P, Access, Data), not allow(P, Access, Data).
This is not a pure Datalog program because it uses negation. But the use of negation in this program has a well-founded semantics [10]. The complexity of a Datalog program with well-founded negation is polynomial in the size of input [6]. In practice the policy checking algorithm runs very efficiently in XSB (see section 7).
We ran our tool on a small network used by seven hundred users. We analyzed a subset of the network that contains only machines managed by the system administrators.4 Our tool found a violation of policy because of a vulnerability. The system administrators subsequently patched the bug.
hacl(internet, webServer, tcp, 80). hacl(webServer, fileServer, rpc, 100003). hacl(webServer, fileServer, rpc, 100005). hacl(fileServer, AnyHost, AnyProtocol, AnyPort). hacl(workStation, AnyHost, AnyProtocol, AnyPort). hacl(H, H, AnyProtocol, AnyPort).
The following Datalog tuples describe the configuration information of the three machines.
networkService(webServer , httpd, tcp , 80 , apache). nfsMount(webServer, '/www', fileServer, '/export/www'). networkService(fileServer, nfsd, rpc, 100003, root). networkService(fileServer, mountd, rpc, 100005, root). nfsExport(fileServer, '/export/share', read, workStation). nfsExport(fileServer, '/export/www', read, webServer). nfsMount(workStation, '/usr/local/share', fileServer, '/export/share').
The fileServer serves files for the webServer and the workStation through the NFS protocol. There are actually many machines represented by workStation. They are managed by the administrators and run the same software configuration. To avoid the hassle of installing each application on each of the machines separately, the administrators maintain a collection of application binaries under /export/share on fileServer so that any change like recompilation of an application program needs to be done only once. These binaries are exported through NFS to the workStation. The directory /export/www is exported to webServer.
dataBind(projectplan, workStation, '/home'). dataBind(webPages, webServer, '/www').
hasAccount(user, workStation, userAccount). hasAccount(sysAdmin, workStation, root). hasAccount(sysAdmin, webServer, root). hasAccount(sysAdmin, fileServer, root). hasAccount(attacker, internet, root). malicious(attacker).
allow(Anyone, read, webPages). allow(user, AnyAccess, projectPlan). allow(sysAdmin, AnyAccess, Data).
vulExists(workStation, 'CAN-2004-0427', kernel). vulExists(workStation, 'CAN-2004-0554', kernel). vulExists(workStation, 'CAN-2004-0495', kernel). vulExists(workStation, 'CVE-2002-1363', libpng).
The MulVAL reasoning engine then analyzed this output in combination with the other inputs described above. The tool did indeed find a policy violation because of the bug CVE-2002-1363 -- a remotely exploitable bug in the libpng library. A reasoning rule for remote exploit derives that the workStation machine can be compromised. Thus the projectPlan data stored on it can be accessed by the attacker, violating the policy. Our system administrators subsequently patched the vulnerable libpng library.
One might be curious that there was only one vulnerability that contributed to the policy violation though the host workStation actually had four vulnerabilities. The other three bugs on the workStation are locally exploitable vulnerabilities in the kernel. Since only trusted users access these hosts, after patching the libpng bug our tool indicates the policy is no longer violated. These machines have uptimes in the order of months and upgrading the kernel would require a reboot. Patching these vulnerabilities would result in a loss of availability, which is best avoided. The administrators can meet the security goals without patching the kernel and rebooting the workStation. We expect our tool to be useful in mission-critical systems like commercial mail servers serving millions of users and servers running long computations.
vulExists(webServer, 'CVE-2002-0392', httpd). vulExists(fileServer, 'CAN-2003-0252', mountd).
Both vulnerabilities are remotely exploitable and can result in privilege escalation. The corresponding Datalog clauses from ICAT database are:
vulProperty('CVE-2002-0392', remoteExploit, privEscalation). vulProperty('CAN-2003-0252', remoteExploit, privEscalation).
The machine and network configuration, principal and data binding, and the security policy are the same as in the previous example.
The MulVAL reasoning engine analyzed the input Datalog tuples. The Prolog session transcript is as follows:
| ?- policyViolation(Adversary, Access, Resource). Adversary = attacker Access = read Resource = projectPlan; Adversary = attacker Access = write Resource = webPages; Adversary = attacker Access = write Resource = projectPlan;
We show the trace of the first violation in Appendix A. Here we explain how the attack can lead to the policy violation.
An attacker can first compromise webServer by remotely exploiting vulnerability CVE-2002-0392 to get control of webServer. Since webServer is allowed to access fileServer, he can then compromise fileServer by exploiting vulnerability CAN-2003-0252 and become root on the server. Next he can modify arbitrary files on fileServer. Since the executable binaries on workStation are mounted on fileServer, their integrity will be compromised by the attacker. Eventually an innocent user will execute the compromised client program; this will give the attacker access to workStation. Thus the files stored on it would also be compromised.
One way to fix this violation is moving webPages to webServer and blocking inbound access from dmz zone to internal zone. After incorporating these counter measures, we ran MulVAL reasoning engine on the new inputs and verified that the security policy is satisfied.
bugHyp(webServer, httpd, remoteExploit, privEscalation).The fake bugs are then introduced into the reasoning process.
vulExists(Host, VulID, Prog) :- bugHyp(Host, Prog, Range, Consequence). vulProperty(VulID, Range, Consequence) :- bugHyp(Host, Prog, Range, Consequence).The following Prolog program will determine whether a policy violation will happen with two arbitrary hypothetical bugs.
checktwo(P, Acc, Data, Prog1, Prog2) :- program(Prog1), program(Prog2), Prog1 @< Prog2, cleanState, assert(bugHyp(H1, Prog1, Range1, Conseq1)), assert(bugHyp(H2, Prog2, Range2, Conseq2)), policyViolation(P, Acc, Data).The two assert statements introduce dynamic clauses about hypothetical bugs in two programs (Prolog backtracking will cycle through all possible combination of two programs.). The policy check is conducted with the existence of the dynamic clauses. If no policy violation is found, the execution will back track and another two hypothetical bugs (in different two programs) will be tried. @< is the term comparison operator in Prolog. It ensures a combination of two programs is tried only once. If there exist two programs whose hypothetical bugs will break the security policy of the network, the violation will be reported by checktwo. Otherwise the network can withstand two hypothetical bugs.
We measured the performance of our scanner on a Red Hat Linux 9 host (kernel version 2.4.20-8). The CPU is a 730 MHz Pentium III processor with 128MB RAM. The analysis engine runs on a Windows PC with 2.8GHz Pentium 4 processor with 512MB RAM. We constructed examples with configurations similar to the network in section 5, but with different numbers of web servers, file servers and workstations.
To analyze a network in the MulVAL reasoning engine, one needs to run the
MulVAL scanner on each host and transfer the results to the host running
the analysis engine.
The scanners can execute in parallel on multiple machines.
The analysis engine then operates on the data collected from all hosts.
Since the functioning of the scanner is the same on various hosts,
we measured
the scanner running time on one host. We measured the
running time for the analysis engine for real and synthetic
benchmarks.
The running times (in seconds) are as:
MulVAL scanner | 236 s | |
§5.1 | 0.08 | |
MulVAL | 1 host | 0.08 |
reasoning | 200 hosts | 0.22 |
engine | 400 hosts | 0.75 |
1000 hosts | 3.85 | |
2000 hosts | 15.8 |
MulVAL scanner is the time to run the scanner on
one (typically configured) Linux host; in principle, the
scanner can run on all hosts in parallel. The benchmark
§5.1 is the real-world 3-host network
described in section 5.1. Each benchmark
labeled "n hosts" consists of n similar Linux hosts,
(approximately one third web servers, one-third file servers,
and one-third workstations), with host access rules (i.e.,
firewalls) similar to
§5.1. Our reasoning engine can handle
networks with thousands of hosts in less than a minute.
A typical network might have a dozen kinds of hosts: many web servers, many file servers, many compute servers, many user machines. Depending on network topology and installed software (e.g., are all the web servers in the same place with respect to firewalls, and are they all running the same software?) it may be possible that each group of hosts can be treated as one host for vulnerability analysis, so that n=12 rather than n=12,000. It would be useful to formally characterize the conditions under which such grouping is sound.
To test the speed of our hypothetical analysis, we constructed synthesized networks with different numbers of hosts and different numbers of programs. Each program runs on multiple machines. Since the hypothetical analysis goes through all combination of programs to inject bugs, the running time is dependent on both the number of programs and the number of hypothetical bugs. Figure 3 shows the performance with regard to different number of hosts, number of programs and number of injected bugs. The running time increases with the number of hypothetical bugs, because the analysis engine will need to go through combinations of programs, where n is the number of different kinds of programs and k is the number of injected bugs. k = 0 is the case where no hypothetical bug is injected. The performance degraded significantly with the increase of k . But it still only takes 273 seconds for k = 2 on a network with 1000 hosts and 20 different kinds of programs. Since hypothetical analysis can be performed offline before the existence of a bug is known, it is not important to have fast real-time response time. The degraded performance is acceptable. Figure 3 shows our system can perform this analysis in a reasonable time frame for a big network.
The input size to the MulVAL reasoning engine is:
Data | Source5 | hosts=200 | =2000 |
Data Bind | sys admin | 26 | 3004 lines |
Policy | sys admin | 3 | 3 |
Principal Bind | sys admin | 10 | 10 |
HACL | Smart Firewall | 342 | 3342 |
Scanner Output | OVAL/ICAT | 1222 | 12022 |
OVAL definitions for Red Hat | 202 |
Those with PrivEsc or only DoS | 169 |
Coverage | 84% |
Module | Original | New | ||
OVAL scanner | 13484 | 668 | lines | |
Interaction rules | 393 |
The modularity and simplicity of our design allowed us to effectively leverage the existing tools and databases by writing about a thousand lines of code. We note that the small size and declarative style of our interaction rules makes them easy to understand and debug. The interaction rules model Unix-style security semantics. We foresee that to reason about Windows platforms in addition, the effort involved is comparable. The rules are independent of the vulnerability definitions.
We measured the performance of running the MulVAL scanner in parallel on multiple hosts. We used PlanetLab, a worldwide testbed of over 500 Linux hosts connected via the Internet [20]. We selected 47 hosts in such a way as to get geographical diversity (U.S., Canada, Switzerland, Germany, Spain, Israel, India, Hong Kong, Korea, Japan). We were able to log into 39 of these hosts; of these, we successfully installed the scanner on 33 hosts.6 We ran a script that, in parallel on 33 hosts, opened an SSH session and ran the MulVAL scanner. We assume that many hosts were carrying a normal workload, as we made no attempt to reserve them for this use. The first host responded with data in 1.18 minutes; the first 25 hosts responded within 10 minutes; the first 29 hosts responded within 15 minutes; at this point we terminated the experiment.
For a local area network, we expect fast and uniform response time. But for distributed networks, we recommend that scanning be done asynchronously. Each machine, either when its configuration is known to have changed or periodically, should scan and report configuration information. Then, whenever newly scanned data arrives or whenever new vulnerability data is obtained from OVAL or ICAT, the reasoning engine can be run within seconds.
Currently the MulVAL scanner is implemented by augmenting the standard off-the-shelf OVAL scanner. The OVAL scanner is overloaded with both the task of collecting machine configuration information and the task of comparing the configuration with formal advisories to determine if vulnerabilities exist on a system. The drawback of this approach is that when a new advisory comes, the scanning will have to be repeated on each host. It would be more desirable if the collection of configuration information can be separated from the recognition of vulnerabilities, such that when a new bug report comes, the analysis can be performed on the pre-collected configuration data.
There are also many other issues related to scanning, such as how to deal with errors in configuration files. A full discussion of configuration scanning is out of the scope of this paper.
Suppose that there is a misconfiguration in the sudoers file that lets any user execute any command as user joe. In order to do so the scanner must understand the configuration file sudoers and the interaction rules modeling the behavior of program sudo must be added. In general, we expect that we need to model the normal software behavior of a small number of programs. Although it's easy enough to model new programs using Datalog clauses, a substantial advantage of our approach has been that the set of modeling clauses grows much more slowly than the number of advisories.
There is a long line of work on network vulnerability analysis [27,25,23,24,1,17]. These works did not address how to automatically integrate vulnerability specifications from the bug-reporting community into the reasoning model, crucial for applying the analysis in practice. A major difference between MulVAL and these previous works is that MulVAL adopts Datalog as the modeling language, which makes integrating existing bug databases straightforward. Datalog also makes it easy to factor out various information needed in the reasoning process, which enabling us to leverage off-the-shelf tools and yield a deployable end-to-end system.
Ritchey and Amman proposed using model checking for network vulnerability analysis [23]. Sheyner, et. al extensively studied attack-graph generation based on model-checking techniques [24]. MulVAL adopts a logic-programming approach and uses Datalog in the modeling and analysis of network systems. The difference between Datalog and model-checking is that derivation in Datalog is a process of accumulating true facts. Since the number of facts is polynomial in the size of the network, the process will terminate efficiently. Model checking, on the other hand, checks temporal properties of every possible state-change sequence. The number of all possible states is exponential in the size of the network, thus in the worst case model checking could be exponential. However, in network vulnerability analysis it is normally not necessary to track every possible state change sequence. For network attacks, one can assume the monotonicity property -- gaining privileges does not hurt an attacker's ability to launch more attacks. Thus when a fact is derived stating that an attacker can gain a certain privilege, the fact can remain true for the rest of the analysis process. Also, if at a certain stage an attacker has multiple choices for his next step, the order in which he carries out the next attack steps is irrelevant for vulnerability analysis under the monotonicity assumption. While it is possible that a model checker can be tuned to utilize the monotonicity property and prune attack paths that do not need to be examined, model checking is intended to check rich temporal properties of a state-transition system. Network security analysis requires only a small fraction of model-checking's reasoning power. And it has not been demonstrated that the approach scales well for large networks.
Amman et. al proposed a graph-based search algorithms to conduct network vulnerability analysis [1]. This approach also assumes the monotonicity property of attacks and has polynomial time complexity. The central idea is to use an exploit dependency graph to represent the pre- and postconditions for exploits. Then a graph search algorithm can ``string'' individual exploits and find attack paths involves multiple vulnerabilities. This algorithm is adopted in Topological Vulnerability Analysis (TVA) [13], a framework that combines an exploit knowledge base with a remote network vulnerability scanner to analyze exploit sequences leading to attack goals. However, it seems building the exploit model involves manual construction, limiting the tool's use in practice. In MulVAL, the exploit model is automatically extracted from the off-the-shelf vulnerability database and no human intervention is needed. Compared with a graph data structure, Datalog provides a declarative specification for the reasoning logic, making it easier to review and augment the reasoning engine when necessary.
Datalog has also been used in other security systems. The Binder [7] security language is an extension of Datalog used to express security statements in a distributed system. In D1LP, the monotonic version of Delegation Logic [15], Datalog is extended with delegation constructs to represent policies, credentials, and requests in distributed authorization. We feel Datalog is an adequate language for many security purposes due to its declarative semantics and efficient reasoning.
Modeling vulnerabilities and their interactions can be dated back to the Kuang and COPS security analyzers for Unix [2,8]. Recent works in this area include the one by Ramakrishnan and Sekar [21], and the one by Fithen et al [9]. These works consider vulnerabilities on a single host and use a much finer grained model of the operating system than ours. The goal is to analyze intricate interactions of components on a single host that would render the system vulnerable to certain attacks. The result of this analysis could serve as attack methodologies to be added as interaction rules in MulVAL. Specifically, it is possible that one can write an interaction rule that expresses the attack pre and postconditions without mentioning the details of how the low-level system components interact. These rules can then be used to reason about the vulnerability at the network level. Thus the work on single-host vulnerability analysis is complementary to ours.
MulVAL leverages existing work to gather information needed for its analysis. OVAL [26] provides an excellent baseline method for gathering per-host configuration information. Also, research in the past ten years has yielded numerous tools that can manage network configurations automatically [11,12,3,4]. Although these works do not directly involve vulnerability analysis, they provide a good abstraction for the network model, which is used in MulVAL and simplifies its reasoning process.
Intrusion detection systems have been widely deployed in networks and extensively studied in the literature [5,16,14]. Unlike IDS, MulVAL aims at detecting potential attack paths before an attack happens. The goal of the work is not to replace IDS, but rather to complement it. Having an a priori analysis on the configuration of a network is important from the defense-through-depth point of view. Undoubtedly, the more problems discovered before an attack happens, the better the security of the network.
In this section, we present a trace for the example policy violation discussed in section 5.2. We wrote a meta-interpreter to generate the attack tree and visualize it in plain text or html format. In the future we hope to use XSB's online justifier [19] to dump an attack graph and visualize it.
The trace for one of the policy violation is shown below. Each internal node is attributed with the rule used to derive the node.
|-- policyViolation(attacker,read,projectPlan) |-- dataBind(projectPlan,workStation,/home) |-- accessFile(attacker,workStation,read,'/home') Rule: execCode implies file access |-- execCode(attacker,workStation,root) Rule: Trojan horse installation |-- malicious(attacker) |-- accessFile(attacker,workStation,write,'/sharedBinary') Rule: NFS semantics |-- nfsMounted(workStation,'/sharedBinary',fileServer,'/export',read) |-- accessFile(attacker,fileServer,write,'/export') Rule: execCode implies file access |-- execCode(attacker,fileServer,root) Rule: remote exploit of a server program |-- malicious(attacker) |-- vulExists(fileServer,CAN-2003-0252,mountd,remoteExploit,privEscalation) |-- networkServiceInfo(fileServer,mountd,rpc,100005,root) |-- netAccess(attacker,fileServer,rpc,100005) Rule: multi-hop access |-- execCode(attacker,webServer,apache) Rule: remote exploit of a server program |-- malicious(attacker) |-- vulExists(webServer,CAN-2002-0392,httpd,remoteExploit,privEscalation) |-- networkServiceInfo(webServer,httpd,tcp,80,apache) |-- netAccess(attacker,webServer,tcp,80) Rule: direct network access |-- located(attacker,internet) |-- hacl(internet,webServer,tcp,80) |-- hacl(webServer,fileServer,rpc,100005) |-- localFileProtection(fileServer,root,write,/export) |-- localFileProtection(workStation,root,read,/home) |-- not allow(attacker,read,projectPlan)
This paper was originally published in the
Proceedings of the 14th USENIX Security Symposium,
July 31August 5, 2005, Baltimore, MD Last changed: 3 Aug. 2005 ch |
|