Projekt

Zurück zur Übersicht

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

Titel Englisch Detection of Security Flaws and Vulnerabilities by Guided Model Checking - extension
Gesuchsteller/in Sharygina Natasha
Nummer 122077
Förderungsinstrument Projektförderung (Abt. I-III)
Forschungseinrichtung Facoltà di scienze informatiche Università della Svizzera italiana
Hochschule Università della Svizzera italiana – USI
Hauptdisziplin Mathematik
Beginn/Ende 01.10.2008 - 30.09.2010
Bewilligter Betrag 195'301.00
Alle Daten anzeigen

Keywords (8)

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

Lay Summary (Englisch)

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.
Direktlink auf Lay Summary Letzte Aktualisierung: 21.02.2013

Verantw. Gesuchsteller/in und weitere Gesuchstellende

Mitarbeitende

Verbundene Projekte

Nummer Titel Start Förderungsinstrument
111687 Detection of Security Flaws and Vulnerabilities by Guided Model Checking 01.09.2006 Projektförderung (Abt. 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.
-