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


Download (4MB) | Preview
[error in script] [error in script]
Item Type: Tesi di dottorato
Resource language: English
Title: Model-Based Verification Of Operating Systems Device Drivers
Fucci, Francescofrancesco.fucci@unina.it
Date: 31 March 2015
Number of Pages: 120
Institution: Università degli Studi di Napoli Federico II
Department: 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:
Garofalo, Francescofranco.garofalo@unina.it
Cotroneo, DomenicoUNSPECIFIED
Date: 31 March 2015
Number of Pages: 120
Keywords: 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
Date Deposited: 23 Apr 2015 15:58
Last Modified: 25 Sep 2015 10:22
URI: http://www.fedoa.unina.it/id/eprint/10079
DOI: 10.6092/UNINA/FEDOA/10079

Collection description

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)

View Item View Item