Sécurisation de programmes par contrôleur d'exécution / Program monitoring for security
Prof. Patrick COUSOT
Nous avons montré que les transformations de programmes se
formalisent par interprétation abstraite :
Parmi les exemples de transformations de programmes donnés dans
cet article, nous considérons le contrôle d'exécution
d'un programme P par un moniteur M (“program monitoring”) qui
consiste à transformer le programme P en un programme t[P] dont les
exécutions sont celles de P qui sont autorisées par M. Parmi
les applications de cette technique de contrôle d'exécution,
notons :
- le contrôle qu'un programme satisfait une politique
de sécurité définie comme un ensemble de
suites d'opérations autorisées (spécifié
par une formule d'une logique modale ou un automate),
mais également :
- le test d'erreurs à l'exécution;
- L'ordonnancement d'exécutions parallèles (“static scheduling”);
- Les preuves de programmes par transformation (si P = t[P] alors
P satisfait la politique définie par le moniteur M).
-