Doctorant F/H Vérification de la correction fonctionnelle de composants de systèmes d'exploitation

Operating system code (kernel, device drivers) has become increasingly complex, yet it still involves a

large amount of low level code which manipulates intricate data-structures. Moreover, the stability of the OS

(operating system) is critical for any computing system, due to its role managing the other processes and all the

resources of the machine (CPU, memory, I/O access). Therefore, it is important to check that OS code meets

important correctness properties, such as, in increasing order of difficulty (1) basic safety (absence of runtime

errors), (2) the preservation of structural invariants, and (3) more advanced functional properties (e.g., that a

scheduler correctly implements the intended scheduling algorithm).

Static analysis based on abstract interpretation aims at computing program invariants so as to discharge

the verification of such properties. It is automatic and sound (it never validates a program that is incorrect)

but incomplete, which means that it may fail to prove the correctness of a program that meets the property of

interest. Therefore, the practical design of static analyzers remains a grand challenge. In particular, the design

of expressive and computable families of predicates requires a lot of effort.

In the case of OS code as described above, several families of static analysis have achieved impressive

progress. In particular, shape analysis relies on predicates which describe data-structures of unbounded size in

a compact way, which allows generalizing properties observed over short symbolic executions into expressive

program invariants, for many programs that manipulate complex data-structures. In particular, data-structures

like linked pointer structures (lists and trees), and linear structures (arrays) are well handled by existing shape

analysis techniques.

However, many important issues remain. In particular, OS code often mixes and overlays arrays and linked

structures. Such code often relies on structural patterns that are not so well-covered by existing shape analyses.

If we consider the combinations of arrays and linked-structures, several works (by P. Sotin, J. Liu and X. Rival

[4, 5]) have allowed to describe precisely structures that consist of an array that contains a linked list structure,

however, more complex combinations are not handled by any existing shape analysis. For instance, structures

made of an array the elements of which point to separate linked lists cannot be described by existing abstract

domains. Another poorly handled structural pattern consists of overlaid lists, where large structures are shared

in multiple lists [2].

In this thesis, we propose to design abstract domains for combinations of arrays and linked structures so

as to handle both aforementioned patterns. The design of abstract domains will include the formalization of

abstract elements, of the concretization function, and of the abstract operations. Moreover, we will implement

the proposed abstract domains into the MemCAD static analyzer [1, 3], which is developed in the ANTIQUE

INRIA Research Team, and we will evaluate the implementation based on existing OS code, and assess whether

it can achieve the proof of aforementioned properties (1), (2), and (3). Finally, we expect our study to also

produce generalization of abstract domains used in shape analysis.

Operating system code (kernel, device drivers) has become increasingly complex, yet it still involves a

large amount of low level code which manipulates intricate data-structures. Moreover, the stability of the OS

(operating system) is critical for any computing system, due to its role managing the other processes and all the

resources of the machine (CPU, memory, I/O access). Therefore, it is important to check that OS code meets

important correctness properties, such as, in increasing order of difficulty (1) basic safety (absence of runtime

errors), (2) the preservation of structural invariants, and (3) more advanced functional properties (e.g., that a

scheduler correctly implements the intended scheduling algorithm).

Static analysis based on abstract interpretation aims at computing program invariants so as to discharge

the verification of such properties. It is automatic and sound (it never validates a program that is incorrect)

but incomplete, which means that it may fail to prove the correctness of a program that meets the property of

interest. Therefore, the practical design of static analyzers remains a grand challenge. In particular, the design

of expressive and computable families of predicates requires a lot of effort.

In the case of OS code as described above, several families of static analysis have achieved impressive

progress. In particular, shape analysis relies on predicates which describe data-structures of unbounded size in

a compact way, which allows generalizing properties observed over short symbolic executions into expressive

program invariants, for many programs that manipulate complex data-structures. In particular, data-structures

like linked pointer structures (lists and trees), and linear structures (arrays) are well handled by existing shape

analysis techniques.

However, many important issues remain. In particular, OS code often mixes and overlays arrays and linked

structures. Such code often relies on structural patterns that are not so well-covered by existing shape analyses.

If we consider the combinations of arrays and linked-structures, several works (by P. Sotin, J. Liu and X. Rival

[4, 5]) have allowed to describe precisely structures that consist of an array that contains a linked list structure,

however, more complex combinations are not handled by any existing shape analysis. For instance, structures

made of an array the elements of which point to separate linked lists cannot be described by existing abstract

domains. Another poorly handled structural pattern consists of overlaid lists, where large structures are shared

in multiple lists [2].

In this thesis, we propose to design abstract domains for combinations of arrays and linked structures so

as to handle both aforementioned patterns. The design of abstract domains will include the formalization of

abstract elements, of the concretization function, and of the abstract operations. Moreover, we will implement

the proposed abstract domains into the MemCAD static analyzer [1, 3], which is developed in the ANTIQUE

INRIA Research Team, and we will evaluate the implementation based on existing OS code, and assess whether

it can achieve the proof of aforementioned properties (1), (2), and (3). Finally, we expect our study to also

produce generalization of abstract domains used in shape analysis.

Operating system code (kernel, device drivers) has become increasingly complex, yet it still involves a

large amount of low level code which manipulates intricate data-structures. Moreover, the stability of the OS

(operating system) is critical for any computing system, due to its role managing the other processes and all the

resources of the machine (CPU, memory, I/O access). Therefore, it is important to check that OS code meets

important correctness properties, such as, in increasing order of difficulty (1) basic safety (absence of runtime

errors), (2) the preservation of structural invariants, and (3) more advanced functional properties (e.g., that a

scheduler correctly implements the intended scheduling algorithm).

Static analysis based on abstract interpretation aims at computing program invariants so as to discharge

the verification of such properties. It is automatic and sound (it never validates a program that is incorrect)

but incomplete, which means that it may fail to prove the correctness of a program that meets the property of

interest. Therefore, the practical design of static analyzers remains a grand challenge. In particular, the design

of expressive and computable families of predicates requires a lot of effort.

In the case of OS code as described above, several families of static analysis have achieved impressive

progress. In particular, shape analysis relies on predicates which describe data-structures of unbounded size in

a compact way, which allows generalizing properties observed over short symbolic executions into expressive

program invariants, for many programs that manipulate complex data-structures. In particular, data-structures

like linked pointer structures (lists and trees), and linear structures (arrays) are well handled by existing shape

analysis techniques.

However, many important issues remain. In particular, OS code often mixes and overlays arrays and linked

structures. Such code often relies on structural patterns that are not so well-covered by existing shape analyses.

If we consider the combinations of arrays and linked-structures, several works (by P. Sotin, J. Liu and X. Rival

[4, 5]) have allowed to describe precisely structures that consist of an array that contains a linked list structure,

however, more complex combinations are not handled by any existing shape analysis. For instance, structures

made of an array the elements of which point to separate linked lists cannot be described by existing abstract

domains. Another poorly handled structural pattern consists of overlaid lists, where large structures are shared

in multiple lists [2].

In this thesis, we propose to design abstract domains for combinations of arrays and linked structures so

as to handle both aforementioned patterns. The design of abstract domains will include the formalization of

abstract elements, of the concretization function, and of the abstract operations. Moreover, we will implement

the proposed abstract domains into the MemCAD static analyzer [1, 3], which is developed in the ANTIQUE

INRIA Research Team, and we will evaluate the implementation based on existing OS code, and assess whether

it can achieve the proof of aforementioned properties (1), (2), and (3). Finally, we expect our study to also

produce generalization of abstract domains used in shape analysis.

Compétences techniques et niveau requis :

Langues :

Compétences relationnelles :

Compétences additionnelles appréciées :

• Restauration subventionnée
• Transports publics remboursés partiellement
• Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
• Possibilité de télétravail (après 6 mois d'ancienneté) et aménagement du temps de travail
• Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
• Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
• Accès à la formation professionnelle
• Sécurité sociale