Return to search

RTL-Check: A practical static analysis framework to verify memory safety and more

Puisque les ordinateurs sont omniprésents dans notre société et que, de plus en
plus, nous dépendons de programmes pour accomplir nos activités de tous les jours,
les bogues peuvent parfois avoir des conséquences cruciales. Une grande proportion des
programmes existants sont écrits en C ou en C++ et la plupart des erreurs avec ces
langages sont dues à l’absence de sûreté d’accès à la mémoire. Notre objectif à long
terme est d’être en mesure de vérifier si un programme C ou C++ accède correctement
à la mémoire malgré les défauts de ces langages.
À cette fin, nous avons créé un cadre de développement d’analyses statiques que
nous présentons dans ce mémoire. Il permet de construire des analyses à partir de petits
composants réutilisables qui sont liés automatiquement par métaprogrammation. Il
incorpore également le modèle de conception (design pattern) du visiteur et des algorithmes
utiles pour faire de l’analyse statique. De plus, il fournit un modèle objet pour
le RTL, la représentation intermédiaire de bas niveau pour tous les langages supportés
par GCC. Ceci implique qu’il est possible de concevoir des analyses indépendantes des
langages de programmation.
Nous décrivons également les modules que comporte l’analyse statique que nous
avons développée à l’aide de notre cadre d’analyse et qui vise à vérifier si un programme
respecte les règles d’accès à la mémoire. Cette analyse n’est pas complète, mais elle
est conçue pour être améliorée facilement. Autant le cadre d’analyse que les modules
d’analyse des accès à la mémoire sont distribués dans RTL-Check, un logiciel libre. / Since computers are ubiquitous in our society and we depend more and more on programs
to accomplish our everyday activities, bugs can sometimes have serious consequences.
A large proportion of existing programs are written in C or C++ and the
main source of errors with these programming languages is the absence of memory
safety. Our long term goal is to be able to verify if a C or C++ program accesses
memory correctly in spite of the deficiencies of these languages.
To that end, we have created a static analysis framework which we present in this
thesis. It allows building analyses from small reusable components that are automatically
bound together by metaprogramming. It also incorporates the visitor design
pattern and algorithms that are useful for the development of static analyses. Moreover,
it provides an object model for RTL, the low-level intermediate representation for
all languages supported by GCC. This implies that it is possible to design analyses that
are independent of programming languages.
We also describe the modules that comprise the static analysis we have developed
using our framework and which aims to verify if a program is memory-safe. This analysis
is not yet complete, but it is designed to be easily improved. Both our framework and
our memory access analysis modules are distributed in RTL-Check, an open-source
project.

Identiferoai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2006/23909
Date09 1900
CreatorsLacroix, Patrice
ContributorsDesharnais, Jules
PublisherUniversité Laval
Source SetsLibrary and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada
LanguageEnglish
Detected LanguageFrench
TypeElectronic Thesis or Dissertation
Formattext/html, application/pdf
Rights© Patrice Lacroix, 2006

Page generated in 0.0018 seconds