Code one C Manuel d'utilisateur télécharger pdf

Model Checking One Million Lines of C Code

∗

Hao Chen Drew Dean David Wagner

UC Berkeley SRI International UC Berkeley

[email protected] [email protected] [email protected]

Abstract

Implementation bugs in security-critical software are

pervasive. Several authors have previously suggested

model checking as a promising means to detect improper

use of system interfaces and thereby detect a broad class

of security vulnerabilities. In this paper, we report on

our practical experience using MOPS, a tool for software

model checking security-critical applications. As exam-

ples of security vulnerabilities that can be analyzed using

model checking, we pick ﬁve important classes of vulnera-

bilities and show how to codify them as temporal safety

properties, and then we describe the results of check-

ing them on several signiﬁcant Unix applications using

MOPS. After analyzing over one million lines of code, we

found more than a dozen new security weaknesses in im-

portant, widely-deployed applications. This demonstrates

for the ﬁrst time that model checking is practical and use-

ful for detecting security weaknesses at large scale in real,

legacy systems.

1. Introduction

From the dawn of the computing era, software has per-

formed in ways surprising to its authors. In short: soft-

ware has bugs. Right from the beginning, computer secu-

rity researchers have recognized that assurance would be

a critical challenge for the ﬁeld, and much work has gone

into formal methods for verifying programs. While there

have been some successes in the national security arena,

formal methods have yet to make it into mainstream soft-

ware development, be it commercial or open source. And

so, software in the 21st century still has bugs, and this

seems likely to remain true for the foreseeable future.

All hope, however, is not lost. For instance, a variety

of techniques have recently emerged for dealing with the

lack of memory safety in the C programming language.

Static analysis techniques, with some limitations, can now

∗

This work was supported by the Ofﬁce of Naval Research under con-

tract N00014-02-1-0109, DARPA under contract N66001-00-C-8015,

NSF CCR-0093337, and generous donations from Microsoft and Intel.

handle real world programs. And, model checking has

provided an alternative paradigm to theorem proving in

formal methods.

Model checking has several important advantages. For

one, model checking is particularly useful because it tells

exactly why a property isn’t satisﬁed, rather than leaving

one scratching one’s head trying to ﬁgure out if the formal

proof is failing because the theorem is false, or one is sim-

ply insufﬁciently clever to prove it in the formal system

being used. Also, the advent of model checking has in-

troduced a new spin on formal methods: beyond their ap-

plications for veriﬁcation of systems, model checkers are

even more useful for ﬁnding bugs in systems. Other re-

searchers have reported signiﬁcant advantages to focusing

on bug-checking, at least when looking for non-security

bugs [10], and so the time seems ripe to examine how

model checking might improve software security.

In this paper, we initiate an empirical study of model

checking as a means to improve the security of our soft-

ware. Our aim is to ﬁnd problems in software written

with benign intent; verifying the absence of bugs is ex-

plicitly less important. In this sense, we ﬁt squarely into

Jackson’s “lightweight formal methods” [13]. Hence, al-

though we take a principled approach (model checking),

we are driven more by the pragmatics of checking large

software packages for security issues than by theoretical

arguments.

Many security problems in Unix programs are viola-

tions of folk rules for the construction of secure programs,

especially for setuid programs. Some of these rules

are amenable to simple local checks, such as those per-

formed by ITS4 [20] and RATS [15]. Others, alas, require

searching through all possible control ﬂow paths through

the program. Such analysis is painful and error-prone if

done by hand. We’ve built a tool, called MOPS, which

was designed and implemented to meet the need for au-

tomation to support the security analyst. In this paper,

we report on experience with using MOPS to check six

large, well-known, frequently used, open source packages

(Apache HTTPD, BIND, OpenSSH, Postﬁx, Samba, and

Sendmail) and two small setuid applications (At and Vix-

ieCron) in Red Hat Linux 9.

1 2 3 4 5 6 ... 14 15

Résumé du contenu

Page 1 - 1. Introduction

Model Checking One Million Lines of C Code∗Hao Chen Drew Dean David WagnerUC Berkeley SRI International UC [email protected] [email protected]

Page 2 - 2. Overview of MOPS

An option in the Apache web server httpd lets the serverexecute CGI programs as the program owner (e.g. usingthe owner’s user ID and group ID). Since

Page 3 - 3. Experiments

We are unaware of any way to exploit this bug. Thoughit is possible for an attacker to corrupt the task ﬁle, the at-tacker has little control over the

Page 4

• mops ld: a linker that takes a set of CFG ﬁles andmerges them into a single CFG ﬁle, resolving crossreferences of external functions and variables.•

Page 5

in the future. Take OpenSSH, for example. In version2.5.2p2, ssh drops all privileges permanently by callingsetuid(getuid()). In the newer version 3.5

Page 6 - 3.3. Performance

ties in C/C++ programs. It uses a global context-sensitive,control-ﬂow-insensitive analysis in the ﬁrst phase and aninter-procedural,context-sensitive

Page 7 - 3.4. Usability

[18] U. Shankar, K. Talwar, J. S. Foster, and D. Wagner. De-tecting format string vulnerabilities with type qualiﬁers.In Proceedings of the 10th USENI

Page 8

We have found previously unknown weaknesses in ﬁveout of the eight programs that we checked. Our experiencehas demonstrated that model checking securi

Page 9 - 4. Findings

MOPS is unsuitable for checking concurrent pro-grams.• The program is memory safe, e.g., no buffer over-runs.• The program is portable. For instance,

Page 10

calls are safe. So we check the following property, whichis a good approximation of the desired behavior (see Fig-ure 2):Property 1 A process should d

Page 11 - 5. Experience and Lessons

ruid=0,euid!=0,suid=0ruid=0,euid=0,suid=0ruid!=0,euid!=0,suid!=0ruid=0,euid!=0,suid!=0ruid!=0,euid=0,suid=0ruid=0,euid=0,suid!=0ruid!=0,euid=0,suid!=0

Page 12 - 5.3. Value of Tool Support

stat(f)open(f)rename(f, *)...other otherstat(f)open(f)rename(f, *)...(a) An FSA describing Property 3stat(logﬁle, &st);if (st.stuid != getuid())re

Page 13 - 6. Related Work

Program LOC DescriptionApache 2.0.40-21 229K An HTTP serverAt 3.1.8-33 6K A program to queue jobs for later executionBIND 9.2.1-16 279K An implementat

Page 14 - References

Package LOC Pro- Time Error Tracesgrams (m:s) Real TotalApache 229K 2 :45 1 4At 6K 2 :05 0 0BIND 279K 1 :53 0 1OpenSSH 59K 3 :23 2 8Postﬁx 94K 3 :17 0

Page 15

unique programming error. This improvement greatly re-duced the number of error traces that we had to examinemanually in Figure 7.To evaluate the usab

Plus de documents pour Détecteurs de fumée Code one C

Voir le document Code one C Manuel d'utilisateur

Code one C Manuel d'utilisateur (4 pages)

Commentaires sur ces manuels

Pas de commentaire

Code one C Manuel d'utilisateur

Naviguer en ligne ou télécharger Manuel d'utilisateur pour Détecteurs de fumée Code one C. Model Checking One Million Lines of C Code Manuel d'utilisatio

Résumé du contenu

Plus de documents pour Détecteurs de fumée Code one C

Commentaires sur ces manuels

Produits connexes et manuels pour Détecteurs de fumée Code one C