splintchecker.github.io/icse-position.html at master · splintchecker/splintchecker.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
<html>
<head>
<link rel="stylesheet" type="text/css" href="http://www.cs.virginia.edu/~evans/simple.css" title="style1">
<title>Annotation-Assisted Lightweight Static Checking</title>
</head>
<body bgcolor="#FFFFFF">

<center>
<h2>Annotation-Assisted Lightweight Static Checking</h2>
<b>Position Paper for
<a href="http://ase.arc.nasa.gov/icse2000/">
The First International Workshop on Automated Program Analysis, Testing and Verification</a></b><br>
<br>
<b><a href="http://www.cs.virginia.edu/~evans/">David Evans</a></b><br>
<a href="mailto:evans@cs.virginia.edu"><em>evans@cs.virginia.edu</em><br>
<a href="http://www.cs.virginia.edu">University of Virginia, Department of Computer Science</a>
</center>
<p>
Also available as <a href="http://lclint.cs.virginia.edu/patv00.ps">Postcript</a>.

<p>
<h3>
Abstract</h3>

While heavyweight formal methods have shown much promise in academia
and remarkable success in industrial hardware projects, they are
rarely used in industrial software projects.  There are many reasons
for this [DillRusby96, Hall96, HollowayButler96], of which one of the
most important is the lack of a realistic adoption path between
current development techniques and more formal approaches.  Our
research seeks to provide a few of the steps along that path.  Our
experience so far with LCLint [EGHT94, Evans96] indicates that
lightweight static checking tools may provide an effective way to
introduce formal methods into industrial environments.  <p>

<h3>Background</h3>

There is a huge gap between the amount of effort and expertise
required to use traditional development tools (such as compilers,
integrated development environments, and test scripts) and formal
techniques such as <em>Z</em> specifications, model checking, and
program verification.  On the other hand, a large class of common
programming errors can be detected using simpler techniques.  Our
research explores what can be done with minimal programmer effort,
without requiring substantial changes to traditional development
processes, and with a tool that requires no user interaction and runs
about as fast as a typical compiler.  To do this, we have developed
LCLint, a tool for statically checking C programs.  Our approach is
general enough to use with other source languages (in fact, we have
built a prototype for a similar tool for Java), but we focus primarily
on C for pragmatic reasons: it is a small and simple language, and
still widely used in industry in even security-critical applications.

<p> LCLint provides a first step towards the adoption of formal
techniques and mechanical analysis. If minimal effort is invested
adding annotations to programs, LCLint can perform stronger checks
than can be done by any compiler or standard lint.  Adding these
annotations is the first step on the path to using formal analysis
techniques.  LCLint checking is designed to provide a clear and
cost-effective payoff for any effort spent adding annotations.  Some
of the problems that can be detected by LCLint include: violations of
information hiding; inconsistent modifications of caller-visible
state or uses of global variables; memory management errors
including uses of dead storage and memory leaks; and undefined program
behavior.  LCLint checking is done using simple dataflow analyses.
This means the checking is as fast as a compiler, and LCLint can
easily be introduced into standard development cycles.

<p> As one would expect, LCLint's performance and usability goals
require certain compromises to be made regarding the checking.  In
particular, we believe that it is reasonable to sacrifice soundness
and completeness towards these goals (see [Evans96] for a more
complete justification).  While this would not be acceptable in many
environments, it is a desirable tradeoff in a typical industrial
development environment where cost-effective detection of program bugs is
the overriding goal.  LCLint has been in active use for more than five
years, and has been used by thousands of programmers in both industry
and academia.  <p>


<h3>Current Directions</h3>

Our current work focuses on extending this approach in two directions:
enhancing the functionality of LCLint without relaxing the usability
and efficiency requirements by adding support for user-defined
annotations, and providing the next step toward heavyweight formal
methods by introducing more expressive annotations and automated
run-time checking.

<p>

<b>User-defined Annotations.</b> Currently, LCLint users are limited
to a pre-defined set of annotations and associated checking.  This
works well as long as their programming style is consistent with the
methodology supported by LCLint (e.g., abstract data types implemented
by separate modules, pointers used in a limited systematic way), but
is problematic if they need to check a program that does not adhere to
this methodology.  For example, LCLint provides annotations for
checking storage that is managed using reference counting.  An
annotation is used to denote an integer field of a structure as the
reference count, and LCLint will report inconsistencies if new
pointers to the structure are created without increasing the reference
count, or if the storage associated with the referenced object is not
deallocated when the reference count reaches zero.  If a program
implements reference counting in some other way (for example, by
keeping the reference counts in a separate lookup table), however,
LCLint provides no relevant annotations or checking.  More generally,
applications have application-specific constraints that should be
checkable statically.  These could include value consistency
requirements, event ordering requirements, and global constraints.

<p>

We are investigating extensions to LCLint that address this problem by
supporting user-defined annotations.  Programmers will be able to
invent new annotations, express syntactic constraints on their usage,
and define checking associated with the user-defined annotation in different
contexts.  Our approach is to devise annotations for use in detecting
buffer overflow errors, and then to generalize the checking semantics
associated with those annotations and the annotations already provided
by LCLint in such a way that allows all of the annotations to be
expressed using a general meta-annotation language.
<p>

<b>Towards Heavyweight Formal Techniques.</b> The performance and
usability requirements of LCLint inherently limit the kinds of
checking that can be done as well as the claims that can be made about
a checked program.  We can consider overcoming these limitations by
relaxing these requirements.  One approach would be to require more
complete specifications and use theorem-proving technology to perform
more complex checking.  This is similar to what has been done by the
Extended Static Checking (ESC) project at Compaq SRC [DLNS98].  ESC
uses a theorem proving technology, which enables it to detect a larger
class of errors than can be done by the simple dataflow analyses done
by LCLint.  This, however, increases the costs of the analysis
considerably, and makes it difficult to use ESC on large programs.
<p>

Another approach would be to use a combination of static and run-time
checking.  If LCLint is not able to prove statically that a specified
property holds, it could insert run-time checks to ensure the property
holds at run-time.  This has the considerable disadvantage that an
error may still occur at run-time, but it would allow more complex
properties to be guaranteed without requiring the user expertise and
effort typically required of a program verification system.  Our
experience using Naccio to transform programs to enforce a safety
policy described using a general, high-level language [EvansTwyman99,
Evans99] offers a possible approach to automatically inserting
run-time checking in programs.  A related project is the Assertion
Definition Language (ADL) created by Sun Microsystems, X/Open and the
Information-technology Promotion Agency (an agency of Japan's MITI)
[Sankar93, Obayashi98].  The ADLT tool generates run- time assertions
and test cases from ADL specifications and test data annotations that
provide descriptions of test sets.
<p>

Static checking has numerous well-understood advantages over the
combination of run-time checking and automated testing, but cannot
enforce many useful properties that can be easily enforced using
run-time checking.  We believe that a well-integrated combination of
run-time and static checking is likely to be successful in introducing
heavyweight formal methods into industrial environments.  Our current
efforts are directed towards integrating the lightweight static
checking done by LCLint with run-time checking.

<p>
<h3>Availability</h3>

More information on LCLint and source code and binary releases is
available at <a
href="http://lclint.cs.virginia.edu"><em>http://lclint.cs.virginia.edu</em></a>.


<h3>Acknowledgements</h3>

LCLint grew out of the Larch Project at the MIT Lab for Computer
Science and DEC Systems Research Center the led by John Guttag and Jim
Horning.  The work described in this paper is being done by David
Evans, John Knight and David Larochelle at the University of Virginia.

<h3>References</h3>

<font size=-1>

[DLNS98] David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe. <em>Extended Static Checking</em>. Compaq SRC Research Report #159, December, 1998.
<p>
[DillRushby96] D. Dill and J. Rushby.  <em>Acceptance of Formal Methods: Lessons from Hardware Design</em>.  IEEE Computer, April 1996.
<p>
[EGHT94] David Evans, John Guttag, Jim Horning and Yang Meng Tan. <em>LCLint: A Tool for Using Specifications to Check Code</em>. In Proceedings of the SIGSOFT Symposium on the Foundations of Software Engineering, December 1994.
<p>
[Evans96] David Evans. <em>Static Detection of Dynamic Memory Errors</em>. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation (PLDI '96), Philadelphia, PA, May 1996.
<p>
[EvansTwyman99] David Evans and Andrew Twyman. <em>Policy-Directed Code Safety</em>. In Proceedings of the 1999 IEEE Symposium on Security and Privacy, Oakland, California, May, 1999.
<p>
[Evans99] David Evans. <em>Policy-Directed Code Safety</em>. MIT PhD Thesis, October 1999.
<p>
[Hall96] Anthony Hall. <em>What is the Formal Methods Debate About?</em> IEEE Computer, 29(4):22-23, April 1996.
<p>
[HollowayButler96] C. Michael Holloway and Ricky W. Butler. <em>Impediments to Industrial Use of Formal Methods</em>. IEEE Computer, 29(4):25-26, April 1996.
<p>
[Obayashi98] Masaharu Obayashi, Hiroshi Kubota, Shane P. McCarron, Lionel Mallet. <em>The Assertion Based Testing Tool for OOP: ADL2</em>. International Conference on Software Engineering, Kyoto, April 1998.
<p>
[Sankar93] Sriram Sankar and Roger Hayes. <em>Specifying and Testing Software Components using ADL</em>. Sun Microsystems, 1993.


<hr>
<table width=100%>
<tr>
<td width=10% valign=top>
<img src="http://www.cs.virginia.edu/~evans/uvacs/uva_06.gif" align=center alt="UVa CS" width=57 height=56>
</td>
<td align=left width=45% valign=top>
<font size=-1>
<a href="http://www.cs.virginia.edu/~evans/index.html">David Evans</a><br>
<a href="http://www.cs.virginia.edu/">Department of Computer Science</a><br>
<a href="http://www.virginia.edu/">University of Virginia</a><br>
<a href="http://www.virginia.edu/cville.html">Charlottesville, Virginia 22904</a>
</td>

<td align=right valign=top>
<font size=-1>
<a href="mailto:evans@cs.virginia.edu"><em>evans@cs.virginia.edu</em></a><br>
<a href="http://www.cs.virginia.edu/~evans/address.html">Other Addresses</a><br>
</font>
</td>
</tr>
</table>

</body>
</html>