Fucci, Francesco
(2015)
Model-Based Verification Of Operating Systems Device Drivers.
[Tesi di dottorato]
| Tipologia del documento: |
Tesi di dottorato
|
| Lingua: |
English |
| Titolo: |
Model-Based Verification Of Operating Systems Device Drivers |
| Autori: |
| Autore | Email |
|---|
| Fucci, Francesco | francesco.fucci@unina.it |
|
| Data: |
31 Marzo 2015 |
| Numero di pagine: |
120 |
| Istituzione: |
Università degli Studi di Napoli Federico II |
| Dipartimento: |
Ingegneria Elettrica e delle Tecnologie dell'Informazione |
| Scuola di dottorato: |
Ingegneria dell'informazione |
| Dottorato: |
Ingegneria informatica ed automatica |
| Ciclo di dottorato: |
27 |
| Coordinatore del Corso di dottorato: |
| nome | email |
|---|
| Garofalo, Francesco | franco.garofalo@unina.it |
|
| Tutor: |
| nome | email |
|---|
| Cotroneo, Domenico | [non definito] |
|
| Data: |
31 Marzo 2015 |
| Numero di pagine: |
120 |
| Parole chiave: |
operating systems; device drivers; verification; model; symbolic execution |
| Settori scientifico-disciplinari del MIUR: |
Area 09 - Ingegneria industriale e dell'informazione > ING-INF/05 - Sistemi di elaborazione delle informazioni |
| Aree tematiche (7° programma Quadro): |
TECNOLOGIE DELL'INFORMAZIONE E DELLA COMUNICAZIONE > Macchine "più intelligenti", servizi migliori |
[error in script]
[error in script]
| Depositato il: |
23 Apr 2015 15:58 |
| Ultima modifica: |
25 Set 2015 10:22 |
| URI: |
http://www.fedoa.unina.it/id/eprint/10079 |
| DOI: |
10.6092/UNINA/FEDOA/10079 |
Abstract
Critical systems depend on software more than ever. In particular, off-the-shelf operating systems (OS) have a central role in the development of critical systems. Unfortunately, OS are plagued by software defects that threaten their reliability, since verification techniques are still not enough cost-efficient to prevent such defects. In particular, empirical studies found that defective device drivers are the major cause of failures of operating systems. Therefore, more sophisticated techniques are needed in order to make the verification of device drivers more cost-efficient.
This thesis addresses this problem by proposing three solutions for detecting software defects in device drivers. The thesis first proposes a methodology that enhances symbolic execution with model-based verification. The idea is that the developer provides a model of expected interactions between the device driver, the operating system and the device, based on documentation and domain expertise about the OS and the device. We propose a language (SLANG) and a run-time support (SymCheck) to ease the developer in specifying behavioral models and checking them through symbolic execution.
The second contribution of this thesis is an enhanced platform for improving the speed of symbolic execution. This platform is based on an efficient representation of intermediate code, which can achieve an average speed-up of 3x compared to a state-of-the-art symbolic execution platform.
Finally, this thesis provides an approach for run-time verification of the behavior of device driver. The idea is that device drivers behave correctly in most cases, and that anomalies in their behavior are symptomatic of failures. Therefore, the approach uses failure-free execution traces of the device driver, to extract a model of the expected behavior. Then, this model is used to generate a device driver monitor, which inspects the state of the device driver in order to detect divergences between the expected behavior and the actual one. The proposed approaches have been applied on device drivers from the Windows and Linux OS, showing their applicability and usefulness on real-world off-the-shelf OS.
Downloads per month over past year
Actions (login required)
 |
Modifica documento |
