diff options
Diffstat (limited to 'tex/thesis/introduction/introduction.tex')
| -rw-r--r-- | tex/thesis/introduction/introduction.tex | 95 |
1 files changed, 49 insertions, 46 deletions
diff --git a/tex/thesis/introduction/introduction.tex b/tex/thesis/introduction/introduction.tex index d1b1a39..cf32e3d 100644 --- a/tex/thesis/introduction/introduction.tex +++ b/tex/thesis/introduction/introduction.tex @@ -10,45 +10,53 @@ In today's increasingly technological world, software bugs can have significant consequences, ranging from the relatively minor -frustration caused to average users to causing deaths. There have been -several incidents in recent years in which a bug in a software system -has led directly to injury or death. X-ray machines which provide too -high a dose of radiation, cars which continue to accelerate against -the driver's wishes and other dangerous situations have all come about -as a direct result of software bugs. +frustration caused to average users, to causing deaths. There have +been several incidents in recent years in which a bug in a software +system has led directly to injury or death. X-ray machines which +provide too high a dose of radiation, cars which continue to +accelerate against the driver's wishes and other dangerous situations +have all come about as a direct result of software bugs. Software bugs also have significant financial costs, with Hailpern and Santhanam static that debugging, verification and testing can easily comprise 50\% to 75\% of the total development cost of a -system\cite{Hailpern01softwaredebugging}. +system~\cite{Hailpern01softwaredebugging}. -In order to limit the number of bugs we have it has become commonplace -to employ sophisticated approaches to testing. Many different types of -testing are done to attempt to ensure that software is bug-free. These -tests, although extremely useful, are inherently incapable of +In order to limit the number of bugs in a software system, it has become commonplace +to employ sophisticated testing approaches. Different testing +strategies aim to ensure that a software system is bug-free. These +testing strategies, although extremely useful, are inherently incapable of \emph{guaranteeing} that software is free of bugs. This is especially a problem in critical software systems, such as those found in -aeroplanes or large industrial machinery, where software failure can +aeroplanes or large industrial machinery, where software failures can have catastrophic consequences. -In order to provide a guarantee that software is free of bugs we must -in some way \emph{verify} the software before running it. While it is -possible to write programs in a way that is easier to verify, it is -still a difficult and expensive process to provide verification. - -There has been a continuous stream of research into automatically -analysing programs in order to identify bugs from the late 70s to the -present\cite{CousotCousot77-1,EasyChair:117}. This work is broadly -classed \emph{static analysis} and this thesis contributes to this -work. - -Due to Rice's Theorem\cite{Rice} we know that there is no general way -to statically infer properties of programs. In order to overcome this -many approaches to static analysis have been developed, including the -framework of abstract interpretation presented by Cousot and -Cousot\cite{CousotCousot77-1}. In this framework we consider a program -in a simplified, \emph{abstract}, domain. This allows us to perform a -sound analysis in general at the expense of precision. +In order to provide a guarantee that software is free of bugs we +employ \emph{software verification}, that analyses software without +running it. While it is possible to write programs amenable for +software verification, it is still a difficult and expensive process +to perform verification on a software system. + +There has been a continuous stream of research in +program analysis for finding bugs starting from the late 70s to the +present~\cite{CousotCousot77-1,EasyChair:117}. This work is broadly +categorised as \emph{static program analysis}, and this thesis contributes +to this research area. + +Due to Rice's Theorem~\cite{Rice} we know that it is undecidable to +statically infer properties of programs. In order to overcome this +limitation, many approaches to static analysis have been devised +including the framework of abstract interpretation introduced by +Cousot and Cousot~\cite{CousotCousot77-1}. To overcome the +undecidability issues of static program analysis, a program is +represented in an abstract domain which becomes decidable. A +connection (also known as homomorphism) between the abstract domain +and the concrete domain (actual semantics of the program) is +established. This connection is called a Galois-connection and +provides a proof framework to show that the static program analysis is +a ``sound'' approximation of the semantics. The precision of the +analysis depends on the granularity of the approximation. In general, +more precise program analyses result in higher complexity classes. Two abstract domains which are particularly well-known and useful are those of \emph{interval} and \emph{zones}. The interval abstract @@ -62,29 +70,23 @@ analysis, thereby avoiding false-positives, at the cost of speed. The process of determining appropriate bounds for program variables has traditionally been performed by performing several Kleene iterations, followed by a \emph{widening} and \emph{narrowing}. These -widening and narrowing operators ensure termination, but once again at -the cost of precision. As an alternative to these operators we can, in -some instances, use a game-theoretic approach to compute the abstract -semantics of a program\cite{EasyChair:117}. This approach is less +widening and narrowing operators ensure termination, but at +the cost of precision. As an alternative, we employ in this work +a game-theoretic approach to compute the abstract +semantics of a program~\cite{EasyChair:117}. This approach is less general than widening and narrowing, but performs precise abstract interpretation over zones. -In this thesis we present an implementation of this game-theoretic -algorithm, along with our own enhancements which improve its -performance on real-world data. - - - \section{Contribution} In this thesis we present an implementation of the strategy-iteration based static analyser presented by Gawlitza et -al.\cite{EasyChair:117}. Our implementation has several enhancements +al.~\cite{EasyChair:117}. Our implementation has several enhancements which significantly improve the practical performance of the analyser on real-world programs. -Theoretical contribution: +We present one major theoretical contribution: \begin{enumerate} \item We present a demand-driven strategy improvement algorithm for @@ -92,19 +94,18 @@ Theoretical contribution: $\max$ operators. \end{enumerate} -Systems contribution: +We present several systems contributions: \begin{enumerate} \item We develop a solver for monotonic, expansive equation systems based - on the work of Gawlitza et al.\cite{EasyChair:117} with several + on the work of Gawlitza et al.~\cite{EasyChair:117} with several improvements. \item We analyse the performance of our improved solver on a set of equation systems to demonstrate the effect of our improvements. \item We integrate our solver into the LLVM/Clang - framework\cite{LLVM,LLVM-paper,Clang} to perform analysis over - Zones\cite{mine:padoII}. + framework~\cite{LLVM,LLVM-paper,Clang} to perform analysis over Zones~\cite{mine:padoII}. \item We analyse the performance of our LLVM analysis on various program inputs. @@ -124,3 +125,5 @@ Our implementation is discussed in Chapter \ref{chap:implementation}. We discuss several aspects of our implementation before evaluating the results of our analysis on several programs. + +We draw our conclusion in \ref{chap:conclusion}. |