Project

Back to overview

Detection of Security Flaws and Vulnerabilities by Guided Model Checking - extension

English title Detection of Security Flaws and Vulnerabilities by Guided Model Checking - extension
Applicant Sharygina Natasha
Number 122077
Funding scheme Project funding (Div. I-III)
Research institution Istituto del Software (SI) Facoltà di scienze informatiche
Institution of higher education Università della Svizzera italiana - USI
Main discipline Mathematics
Start/End 01.10.2008 - 30.09.2010
Approved amount 195'301.00
Show all

Keywords (8)

Security; Code Verification; information security; formal verification; model checking; static analysis; security vulnerabilities; intrusion detection

Lay Summary (English)

Lead
Lay summary
Information is an important strategic and operational corporate asset, and, therefore, there is a need to have adequate security measures which can safe-guard sensitive information. This project targets the development of techniques that are exhaustive and formally guarantee the correctness of security properties of the actual implementation given in a language such as ANSI-C. Model Checking, a perfect candidate to fulfill the task, exhaustively explores the entire state-space for violations of a property of interest. However, Model Checking suffers from the state-space explosion problem, i.e., the size of the state-space often exceeds the capacity of the Model Checking tool. The main research challenge when applying Model Checking to large-scale software therefore is to address the scalability problem. We propose to tailor state-space reduction algorithms to the code security domain, and thus, to develop specialized model checking algorithms for detecting security vulnerabilities.During the first half of the project we were able to show that focusing on low-level security properties results in a considerable performance gain in static analysis algorithms. In the second half of the project we are extending this work to model checking algorithms and subsequent refinement of abstract models. Among the methods we are investigating are:a) Performance and precision improvements in alias analysis,b) Abstract counterexample analysis and, based on that, guiding heuristics for model checking algorithms,c) Novel counterexample guided abstraction refinement (CEGAR) algorithms based on new abstract transformers, andd) Extensions to modeling formalisms by introduction of quantified verification conditions and improvements in algorithms for quantified bit-vector arithmetic.
Direct link to Lay Summary Last update: 21.02.2013

Responsible applicant and co-applicants

Employees

Associated projects

Number Title Start Funding scheme
111687 Detection of Security Flaws and Vulnerabilities by Guided Model Checking 01.09.2006 Project funding (Div. I-III)

Abstract

This proposal describes a request for extension of the previously funded SNSF project #200021-111687 on ”detection of security flaws and vulnerabilities by guided model checking”. The first two years of the project resulted in four technical publications (with one paper being currently submitted to the Computer-Aided Verification Conference - the major scientific venue in the area of formal verification) and the development of three tools. The request for extension provides the details of each deliverable. Both technical and experimental results are strong and confirm the feasibility of the original proposal. We believe that future work is required to mature the techniques and to make major improvements in security of information systems. Information is an important strategic and operational corporate asset, and, therefore, there is a need to have adequate security measures which can safeguard sensitive information. This project targets the development of techniques that are exhaustive and formally guarantee the correctness of security properties of the actual implementation given in a language such as ANSI-C. Model Checking, a perfect candidate to fulfill the task, exhaustively explores the entire state-space for violations of a property of interest. However, Model Checking suffers from the state-space explosion problem, i.e., the size of the state-space often exceeds the capacity of the Model Checking tool. The main research challenge when applying Model Checking to large-scale software therefore is to address the scalability problem. We propose to tailor state-space reduction algorithms to the code security domain, and thus, to develop specialized model checking algorithms for detecting security vulnerabilities.During the first half of the project we were able to show that focusing on low-level security properties results in a considerable performance gain in static analysis algorithms. We propose to extend this work to model checking algorithms and subsequent refinement of abstract models. Among the methods we propose to investigate are:a) performance and precision improvements in alias analysis,b) abstract counterexample analysis and, based on that, guiding heuristics for model checking algorithms,c) novel counterexample guided abstraction refinement (CEGAR) algorithms based on new abstract transformers, andd) extensions to modeling formalisms by introduction of quantified verification conditions and improvements in algorithms for quantified bit-vector arithmetic.
-