Fucci, Francesco (2015) Model-Based Verification Of Operating Systems Device Drivers. [Tesi di dottorato]

[img]
Anteprima
Testo
fucci_francesco_27.pdf

Download (4MB) | Anteprima
[error in script] [error in script]
Tipologia del documento: Tesi di dottorato
Lingua: English
Titolo: Model-Based Verification Of Operating Systems Device Drivers
Autori:
AutoreEmail
Fucci, Francescofrancesco.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:
nomeemail
Garofalo, Francescofranco.garofalo@unina.it
Tutor:
nomeemail
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
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.

Actions (login required)

Modifica documento Modifica documento