Security analysis of system code using static typing
Operating system kernels need to manipulate data that comes from user programs through system calls. If it is done in an incautious manner, a security vulnerability known as the Confused Deputy Problem can lead to information disclosure or privilege escalation. The goal of this thesis is to use stat...
Main Author: | |
---|---|
Other Authors: | , , , , |
Format: | Doctoral or Postdoctoral Thesis |
Language: | French |
Published: |
HAL CCSD
2014
|
Subjects: | |
Online Access: | https://tel.archives-ouvertes.fr/tel-01067475 https://tel.archives-ouvertes.fr/tel-01067475/document https://tel.archives-ouvertes.fr/tel-01067475/file/these_archivage_2970115opti.pdf |
id |
ftccsdartic:oai:HAL:tel-01067475v1 |
---|---|
record_format |
openpolar |
spelling |
ftccsdartic:oai:HAL:tel-01067475v1 2023-05-15T18:32:45+02:00 Security analysis of system code using static typing Analyse de sécurité de logiciels système par typage statique Millon, Etienne Algorithmes, Programmes et Résolution (APR) Laboratoire d'Informatique de Paris 6 (LIP6) Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS) Université Pierre et Marie Curie - Paris VI Emmanuel Chailloux 2014-07-10 https://tel.archives-ouvertes.fr/tel-01067475 https://tel.archives-ouvertes.fr/tel-01067475/document https://tel.archives-ouvertes.fr/tel-01067475/file/these_archivage_2970115opti.pdf fr fre HAL CCSD NNT: 2014PA066120 tel-01067475 https://tel.archives-ouvertes.fr/tel-01067475 https://tel.archives-ouvertes.fr/tel-01067475/document https://tel.archives-ouvertes.fr/tel-01067475/file/these_archivage_2970115opti.pdf info:eu-repo/semantics/OpenAccess https://tel.archives-ouvertes.fr/tel-01067475 Autre [cs.OH]. Université Pierre et Marie Curie - Paris VI, 2014. Français. ⟨NNT : 2014PA066120⟩ Security Typing Mémoire Pointeurs utilisateur Linux Isolation Typage Sécurité [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH] info:eu-repo/semantics/doctoralThesis Theses 2014 ftccsdartic 2021-03-21T00:08:28Z Operating system kernels need to manipulate data that comes from user programs through system calls. If it is done in an incautious manner, a security vulnerability known as the Confused Deputy Problem can lead to information disclosure or privilege escalation. The goal of this thesis is to use static typing to detect the dangerous uses of pointers that are controlled by userspace. Most operating systems are written in the C language. We start by isolating Safespeak, a safe subset of it. Its operational semantics as well as a type system are described, and the classic properties of type safety are established. Memory states are manipulated using bidirectional lenses, which can encode partial updates to states and variables. A first analysis is described, that identifies integers used as bitmasks, which are a common source of bugs in C programs. Then, we add to Safespeak the notion of pointers coming from userspace. This breaks type safety, but it is possible to get it back by assigning a different type to the pointers that are controlled by userspace. This distinction forces their dereferencing to be done in a controlled fashion. This technique makes it possible to detect two bugs in the Linux kernel: the first one is in a video driver for an AMD video card, and the second one in the ptrace system call for the Blackfin architecture. Les noyaux de systèmes d'exploitation manipulent des données fournies par les programmes utilisateur via les appels système. Si elles sont manipulées sans prendre une attention particulière, une faille de sécurité connue sous le nom de Confused Deputy Problem peut amener à des fuites de données confidentielles ou l'élévation de privilèges d'un attaquant. Le but de cette thèse est d'utiliser des techniques de typage statique afin de détecter les manipulations dangereuses de pointeurs contrôlés par l'espace utilisateur. La plupart des systèmes d'exploitation sont écrits dans le langage C. On commence par en isoler un sous-langage sûr nommé Safespeak. Sa sémantique opérationnelle et ... Doctoral or Postdoctoral Thesis The Pointers Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) |
institution |
Open Polar |
collection |
Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) |
op_collection_id |
ftccsdartic |
language |
French |
topic |
Security Typing Mémoire Pointeurs utilisateur Linux Isolation Typage Sécurité [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH] |
spellingShingle |
Security Typing Mémoire Pointeurs utilisateur Linux Isolation Typage Sécurité [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH] Millon, Etienne Security analysis of system code using static typing |
topic_facet |
Security Typing Mémoire Pointeurs utilisateur Linux Isolation Typage Sécurité [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH] |
description |
Operating system kernels need to manipulate data that comes from user programs through system calls. If it is done in an incautious manner, a security vulnerability known as the Confused Deputy Problem can lead to information disclosure or privilege escalation. The goal of this thesis is to use static typing to detect the dangerous uses of pointers that are controlled by userspace. Most operating systems are written in the C language. We start by isolating Safespeak, a safe subset of it. Its operational semantics as well as a type system are described, and the classic properties of type safety are established. Memory states are manipulated using bidirectional lenses, which can encode partial updates to states and variables. A first analysis is described, that identifies integers used as bitmasks, which are a common source of bugs in C programs. Then, we add to Safespeak the notion of pointers coming from userspace. This breaks type safety, but it is possible to get it back by assigning a different type to the pointers that are controlled by userspace. This distinction forces their dereferencing to be done in a controlled fashion. This technique makes it possible to detect two bugs in the Linux kernel: the first one is in a video driver for an AMD video card, and the second one in the ptrace system call for the Blackfin architecture. Les noyaux de systèmes d'exploitation manipulent des données fournies par les programmes utilisateur via les appels système. Si elles sont manipulées sans prendre une attention particulière, une faille de sécurité connue sous le nom de Confused Deputy Problem peut amener à des fuites de données confidentielles ou l'élévation de privilèges d'un attaquant. Le but de cette thèse est d'utiliser des techniques de typage statique afin de détecter les manipulations dangereuses de pointeurs contrôlés par l'espace utilisateur. La plupart des systèmes d'exploitation sont écrits dans le langage C. On commence par en isoler un sous-langage sûr nommé Safespeak. Sa sémantique opérationnelle et ... |
author2 |
Algorithmes, Programmes et Résolution (APR) Laboratoire d'Informatique de Paris 6 (LIP6) Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS) Université Pierre et Marie Curie - Paris VI Emmanuel Chailloux |
format |
Doctoral or Postdoctoral Thesis |
author |
Millon, Etienne |
author_facet |
Millon, Etienne |
author_sort |
Millon, Etienne |
title |
Security analysis of system code using static typing |
title_short |
Security analysis of system code using static typing |
title_full |
Security analysis of system code using static typing |
title_fullStr |
Security analysis of system code using static typing |
title_full_unstemmed |
Security analysis of system code using static typing |
title_sort |
security analysis of system code using static typing |
publisher |
HAL CCSD |
publishDate |
2014 |
url |
https://tel.archives-ouvertes.fr/tel-01067475 https://tel.archives-ouvertes.fr/tel-01067475/document https://tel.archives-ouvertes.fr/tel-01067475/file/these_archivage_2970115opti.pdf |
genre |
The Pointers |
genre_facet |
The Pointers |
op_source |
https://tel.archives-ouvertes.fr/tel-01067475 Autre [cs.OH]. Université Pierre et Marie Curie - Paris VI, 2014. Français. ⟨NNT : 2014PA066120⟩ |
op_relation |
NNT: 2014PA066120 tel-01067475 https://tel.archives-ouvertes.fr/tel-01067475 https://tel.archives-ouvertes.fr/tel-01067475/document https://tel.archives-ouvertes.fr/tel-01067475/file/these_archivage_2970115opti.pdf |
op_rights |
info:eu-repo/semantics/OpenAccess |
_version_ |
1766216927155322880 |