Back
Texte intégral
Doctoral thesis

Scalable abstractions for efficient security checks

    23.02.2011

151 p

Thèse de doctorat: Università della Svizzera italiana, 2011

Abstraction
Abstraction-refinement loop
Over-approximation
Invariants
Loop invariants
Transition invariants
Termination
Infinite loops
Static analysis
Symbolic execution
English Following the industrial demand to address the problem of software correctness, the computer science research community puts a lot of efforts into development of scalable and precise formal methods that are applicable to industrial-size programs. Unfortunately, most of software verification techniques suffer from the effect of combinatorial blowup also known as a "state-space explosion", i.e., situation, when the size of the system state space and, consequently, the complexity of the verification problem grows exponentially in the size of the input program. This thesis tackles this problem by development of new abstraction techniques as well as novel approaches of employing already existing ones. The results were used to construct algorithms for software verification and static analysis that discover security faults in low-level C programs. First, this thesis presents a new algorithm that combines precise (but slow)} abstraction method with over-approximated (but fast) one in the abstraction-refinement loop. It starts with the coarse over-approximated abstraction and then refines precisely, but restricts the refinement only to a subset of system state space that is related to a spurious counter-example discovered in the previous verification step of the abstraction-refinement loop. Thus, it is possible to keep the refinement computational burden low and decrease the number of required refinement iterations at the same time. We also propose a threshold-based optimization that further controls precise computation in order to avoid the unnecessary application of expensive quantifier elimination. Second, this work defines a new technique for program abstraction. Unlike traditional program approximation approaches (e.g., abstract interpretation) it does not employ iterative fixpoint computation, instead it uses a new summarization algorithm that non-iteratively computes symbolic abstract transformers with respect to a set of abstract domains. Summaries are shorter, loop-free program fragments, which are used to substitute the original loops to obtain a conservative abstraction of the program. Our approach computes abstract transformers starting from the inner-most loop. It obtains a loop invariant by checking if the constraints defined by a chosen abstract domain are preserved by the loop. These checks are performed by means of calls to a quantifier-free decision procedure, which allows us to check (possibly infinite) sets of states with one query. Thus, unlike other approaches, our algorithm is not restricted to finite-height domains.Therefore, it allows for effective usage of problem-specific abstract domains for summarization and, as a consequence, precision of an abstract model can be tuned for specific verification needs. In particular, several memory operations-related abstract domains were applied to perform static analysis of programs for buffer overflows. Third, this thesis addresses the problem of scalable program termination analysis. Termination of a (sequential) program can be concluded from termination of all its loops. Existing algorithms rely on iterative enumeration of all paths through a program (loop) and construction of a valid termination argument (well-founded transition invariant) for each of them using available ranking discovery methods. Instead, we present a new algorithm that applies relational abstract domains for loop summarization to discover transition invariants. Well-foundedness can be ensured either by separate decision procedure call (though it requires quantifier elimination) or by using the abstract domains that are well-founded by construction.Such a light-weight approach to termination analysis was demonstrated to be effective on a wide range of benchmarks, including the OS device drivers.
Language
  • English
Classification
Computer science and technology
License
License undefined
Identifiers
Persistent URL
https://n2t.net/ark:/12658/srd1318314
Statistics
Document views: 144 File downloads:
  • 2011INFO008.pdf: 140