Scalable Abstractions for Efficient Security Checks

Decanato - Facoltà di scienze informatiche

Data d'inizio: 23 Febbraio 2011

Data di fine: 24 Febbraio 2011

You are cordially invited to attend the PhD Dissertation Defense of Aliaksei TSITOVICH on Wednesday, February 23rd 2011 at 11h00 in room 351 (Main building)

Following the industrial demand to address the problem of software correctness, 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” — 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 the 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 the 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.

Dissertation Committee:

  • Prof. Natasha Sharygina, Università della Svizzera italiana, Switzerland (Research Advisor)
  • Prof. Fernando Pedone, Università della Svizzera italiana, Switzerland (Internal Member)
  • Prof. Mauro Pezzè, Università della Svizzera italiana, Switzerland (Internal Member)
  • Prof. Orna Grumberg, Technion Haifa, Israel (External Member)
  • Dr. K. Rustan M. Leino, Microsoft Research Lab, USA (External Member)