Source Code Analysis Techniques in Property Verification of Real Java Code

Szybki rozwój przemysłu komputerowego wymaga budowy coraz potężniejszych i coraz bardziej skomplikowanych systemów, które potrzebują bardzo zaawansowanego i złożonego oprogramowania. Niesie to ze sobą rosnące prawdopodobieństwo wystąpienia błędów. Różne techniki weryfikacji programów są stosowane do zwiększenia jakości oprogramowania. Niestety, techniki wykorzystujące metody formalne nie są zbyt popularne, ponieważ uważa się je za niepraktyczne i drogie. Zastosowanie metod formalnych jest ograniczone do weryfikacji systemów zwiększonego ryzyka, takich jak oprogramowanie sterujące elektrownią jądrową czy oprogramowanie kontroli lotu w samolotach. Podstawowym celem niniejszej rozprawy doktorskiej jest stworzenie techniki analizy statycznej opartej na metodach formalnych, którą można stosować na rzeczywistych programach pisanych w języku Java. Poruszono trzy zagadnienia. Najpierw skoncentrowano się na technikach abstrakcyjnej interpretacji, która jest teorią przybliżania semantyki programu. W szczególności rozważane są numeryczne dziedziny abstrakcyjne. Zaproponowano nowe spojrzenie na dziedzinę pudełek, która jest dysjunktywnym rozszerzeniem dziedziny przedziałów, oraz zastosowano techniki punktów progowych w operatorze rozszerzającym dla tej dziedziny. Przedstawiono konstrukcję elementów dziedziny pudełek bazującą na technice zamiatania wraz z operacjami kratowymi, funkcją transferu i operatorem rozszerzającym. Wprowadzono dwie wersje operatora rozszerzającego: pierwszą ogólną, drugą z twierdzeniem o precyzji jednego kroku rozszerzania uzależnionej od punktów progowych. Następnie skupiono się na praktyczności metod formalnych. Przedstawiono narzędzie CodeStatistics, które służy to wyszukiwania wzorców w kodzie źródłowym Javy i umożliwia generowanie specyfikacji. Zostało ono z sukcesem wykorzystane do wygenerowania warunków terminacji pętli w formacie klauzul decreases języka JML na zestawie dużych, popularnych projektów. Na koniec zaprezentowano rozszerzenie techniki wyszukiwania wzorców będącej przedmiotem rozważań etapu poprzedniego, o techniki analizy semantycznej, w szczególności abstrakcyjnej interpretacji. Wykazano, że połączenie takie może zostać praktycznie zastosowane do oceny dziedzin abstrakcyjnej interpretacji na rzeczywistych programach. Ponadto pokazano, że nowy operator rozszerzający z części pierwszej daje wyniki dokładniejsze niż dotychczas znany.

The rapid growth of computer industry requires creating large, highly complicated and sophisticated software. This implies increasing probability for errors, bugs and failures. Various software verification techniques are used to ensure quality of produced programs. Unfortunately, verification using formal methods is not very popular, because it is considered not practical and expensive. Therefore, formal methods are used to verify only high risk programs, such as control software for nuclear power plants or flight control software in airplanes. The goal of this thesis is to design a static analysis technique that uses formal methods and can be applied to real, large computer software created in Java language. Three topics were raised. First, the thesis focuses on the abstract interpretation framework, which is a theory of sound approximation of program semantics. In particular, we are interested in numerical abstract domains. We propose a new approach on the abstract domain of boxes, which is a disjunctive refinement of the domain of intervals, and we introduce thresholds in the construction of the widening operator for the domain. We present a construction of domain elements based on the sweeping line technique, implementation of domain operators, transfer function and widening operator. We introduce two versions of the widening operator: a generic one, and the second one with a theorem about one-step precision of the operator depending on thresholds. Next, practicality of formal methods is investigated. A tool CodeStatistics is introduced, that makes it possible to discover particular coding patterns on large Java projects and to generate specifications. An experiment is described, where the tool was successfully used to generate JML loop termination specifications on a set of large and popular Java projects. Finally, an extension of the pattern discovery technique from the second part by the use of a semantic analysis is presented, in particular by abstract interpretation. It is shown that the combination is useful in evaluating abstract interpretation domains on real code. Additionally, it is presented that the new widening operator introduced in the first part of the thesis is more precise in practice than the one known so far.