Uncategorized

Detection of Security Flaws and Vulnerabilities by Guided Model Checking

mcWebAdmin — Sun, 02 Dec 2007 03:45:52 +0100

Modern information-driven society has an obvious need for security measures that can safeguard the storage and transfer of sensitive information. Software is responsible for almost 100% of the data manipulation in the world and, thus, should be placed under particularly strict security control. Unfortunately, writing a program devoid of bugs is still one of the greatest challenges for developers. As a result, low level implementation mistakes lead not only to software malfunction, but also to security breaches.

Automated Invariant Discovery for Array-based Systems

Francesco — Tue, 17 Jan 2012 15:22:45 +0100

The research problem addressed by this project is the development of techniques and tools for automated discovering of loop invariants. Infinite program fragments such as loops or recursive functions should be represented by a finite summary, i.e., an invariant, in order to succeed in their verification. Moreover, retrieving an invariant it’s mandatory if we want to model check function handling unbounded data structures (e.g., a function that sorts an input array of unknown length). Such invariants are represented as quantified formulae over the variables of the program.

Formal verification of software changes and upgrades

mcWebAdmin — Tue, 18 Oct 2011 10:49:08 +0200

The project addresses the problem of checking of software upgrades. Serving this goal, state-of-the-art model checkers hardly use the information of the old version, and reduce it thereby to the standalone verification. The purpose of the research is to develop a new technique for checking the software upgrades based on successful verification of the old program and reuse of the invested effort.

The Synergy of Precise and Fast Abstractions for Program Veriﬁcation

mcWebAdmin — Sun, 19 Oct 2008 04:11:45 +0200

Predicate abstraction is a powerful technique to reduce the state space of a program to a finite and affordable number of states. It produces a conservative over-approximation where concrete states are grouped together according to the predicates. Given a set of predicates, a precise abstraction contains the minimal set of transitions, but as a result is computationally expensive. Most model checkers therefore approximate the abstraction to alleviate the computation of the abstract system by trading off precision with cost.

Automated Verification of Security Policies in Mobile Code

mcWebAdmin — Tue, 16 Sep 2008 19:59:52 +0200

This project defines a model checking-based approach for verification of mobile programs against security policies.

Formal Verification via Boolean and Theory Reasoning (SMT)

Roberto — Mon, 21 Jan 2008 10:43:31 +0100

State-of-the-art techniques used in Formal Verification ultimately rely on the expression of properties (of the system to verify) in terms of languages that can be easily understood and processed by automatic tools.