Prévention de fuites d’information dans des applications
interactives
Andrew Bedford, Stephen Chong, Josée Desharnais, Scott Moore,
Nadia Tawbi
Université Laval & Harvard University

Février 2015

Andrew Bedford (Université Laval)

Prévention de fuites

Février 2015

1 / 20La sécurité

Quand est-ce qu’un programme est ”sécuritaire” ?
Confidentialité
Intégrité
I Disponibilité
II

C’est important quelque soit l’application (blog, banque, centrale
nucléaire, ...) !
Des milliards de dollars sont investis à chaque annéeEt pourtant...

Andrew Bedford (Université Laval)

Prévention de fuites

Février 2015

2 / 20Quelques statistiques(Web Application Security Consortium, 2008)

Andrew Bedford (Université Laval)

Prévention de fuites

Février 2015

3 / 20Injection SQL - Exemple

statement = " SELECT * FROM users WHERE name = ’ " + userName +" ’; "userName = " ’ or ’1 ’= ’1 "-->
SELECT * FROM users WHERE name = ’’ OR ’1 ’= ’1 ’;
userName = "a ’; DROP TABLE users ; SELECT * FROM userinfo
WHERE ’t ’ = ’t ’; "-->
SELECT * FROM users WHERE name = ’a ’; DROP TABLE users ;SELECT * FROM userinfo WHERE ’t ’ = ’t ’;

Flot d’information de l’utilisateur à la base de donnéeAndrew Bedford (Université Laval)

Prévention de fuites

Février 2015

4 / 20Cross-site scripting (XSS) - Exemple
Par l’URL :http ://www.a-video-site.org ?q=keyboard cat
Results for ”keyboard cat”

? q = < script t y p e = ’ text / javascript ’ > alert ( ’ MOUAHAHAHAHAH ’); </ script >Partout où on génère du HTML à partir d’une entrée d’un utilisateur(post dans un forum, une signature, un nom d’utilisateur, ...)
Andrew Bedford (Université Laval)

Prévention de fuites

Février 2015

5 / 20Quelques observations

1

En ce moment, c’est au développeur à qui revient la responsabilité deprendre en compte ces flots d’informations

2

Une seule faille peut compromettre tout le système3

La complexité et l’envergure des applications ne cesse d’augmenter

Ce qu’il nous faut : des outils nous permettant de détecter et prévenir
automatiquement ce genre de failles de sécurité !

Andrew Bedford (Université Laval)

Prévention de fuites

Février 2015

6 / 20Notre travail
Afin de pouvoir éventuellement construire de tels outils, nous avons choisitd’étudier comment on pourrait détecter et prévenir les fuites
d’informations dans un petit language impératif intéractif.
(variables)x∈ V(nombres entiers)n ∈ Z(canaux)ch ∈ C(expressions)e ::= x | n | ch | e1 op e2(commandes)c ::= skip | x := e | c1 ; c2 |if e then c1 else c2 end |while e do c end |receive x1 from x2 | send x1 to x2
Notes : On utilise 0 pour faux et non-zéro pour vrai. Les programmes
communiquent uniquement à travers des canaux de communication(fichier, clavier, écran, connection réseau, utilisateur, etc.).
Andrew Bedford (Université Laval)

Prévention de fuites

Février 2015

7 / 20Exemples de fuites(* Flots explicites non - securitaires *)send password t o publicHTML ;x := password + 1010101;
send x t o publicHTML ;i f privateValue > 0 then(* Flot implicite non - securitaire *)send 42 t o publicChannel
end

Lorsque privateValue > 0, publicChannel = [42]Lorsque privateValue <= 0, publicChannel = []Andrew Bedford (Université Laval)

Prévention de fuites

Février 20158 / 20Exemple de fuites

Vu que notre approche étudie les programmes intéractifs, elle doit être
sensible au progrès.
send 0 t o publicFile ;r e c e i v e secretValue from topSecretFile ;w h i l e secretValue >= 0 dos k i p (* Boucle infinie *)end ;send 1 t o publicFile (* Fuite *)Lorsque secretValue >= 0, publicFile = [0]Lorsque secretValue < 0, publicFile = [0,1]Andrew Bedford (Université Laval)

Prévention de fuites

Février 2015

9 / 20Problème : Comment prévenir ces fuites ?
En utilisant le contrôle de flots d’information ! L’idée de base est d’associerà l’information elle-même une étiquette correspondant à son niveau desécurité et de la propager. On utilise :L (Low ) : Pour l’information publicH (High) : Pour l’information privéeU (Unknown) : Pour l’information de niveau inconnu statiquementr e c e i v e x from publicFile ; (* x est L *)r e c e i v e x from topSecretFile ; (* x est H *)y := x + 5; (* y est H *)x := 0; (* x est L *)i f randomValuethen c := publicFile (* c est un canal L *)e l s e c := topSecretFile (* c est un canal H *)end ;r e c e i v e z from c (* z est U ( statiquement ) *)Andrew Bedford (Université Laval)

Prévention de fuites

Février 201510 / 20

Le contrôle de flots d’information

Pour éviter les fuites, on applique une politique de sécurité appelée lanon-interférence.

Définition(Non-interférence) On dit qu’un programme est non-interférent lorsquel’information confidentielle n’affecte pas le comportement public dusystème (dans notre cas, les outputs aux canaux publics). Si un
programme ne respecte pas cette propriété, alors on dira que ce
programme a une fuite d’information.
Confidentialité : Information H 6→ Sorties de niveau LIntégrité : Information L 6→ Sorties de niveau H

Andrew Bedford (Université Laval)

Prévention de fuites

Février 201511 / 20

On applique cette politique en utilisant un système de type.
1

Si le code ne contient pas de fuites évidentes, alors il est instrumenté.
C’est-à-dire qu’il est traduit dans un language cible supportant desvariables étiquettes et des commande sont insérées pour ”tracker” etcontrôler les flots d’informations lors de l’exécution.

2

Le code est ensuite évalué partiellement (optimisation)

Andrew Bedford (Université Laval)

Prévention de fuites

Février 201512 / 20

Andrew Bedford (Université Laval)

Prévention de fuites

Février 201513 / 20Γ est un environnement de typage (map les variables à leur types)
x := 0; (*Γ(x) = intL *)r e c e i v e x from secretFile ; (*Γ(x) = intH *)c := secretFile (*Γ(c) = (intH chan)L *)pc est le program context, une variable niveau. Il permet de détecter
les fuites implicites Il représente le contexte dans lequel on est
présentement.
(*pc = L*)i f privateValue then(*pc = H *)send 42 t o publicChannelendhc est le halting context, une variable niveau. Il permet de détecter
les fuites par progrès. Il représente le niveau d’information qui aurait
pu halter le progrès du programme. En d’autres mots, ...
Afin de pouvoir mettre à jour le hc, chaque commande à un type determinaison qui lui est associé.
Andrew Bedford (Université Laval)

Prévention de fuites

Février 201514 / 20

Les types de terminaisons sont les suivants {T , D, ML , MU , MH }. Où :
T :
D :
ML :
MH :
MU :

si la commande termine toujours
si la commande diverge toujours
si la terminaison de la commande est inconnue statiquement
mais dépend seulement d’information de niveau L
si la terminaison de la commande est inconnue statiquement
mais dépend seulement d’information de niveau H
si la terminaison de la commande est inconnue statiquement
mais dépend à la fois d’information de niveau U.

Andrew Bedford (Université Laval)

Prévention de fuites

Février 201515 / 20

Exemple de terminaisons
x := 1; (* T *)(*hc = L*)send 1 t o publicChannel
w h i l e 1 do s k i p end ; (* D *)(*hc = L*)send secret t o publicChannel
w h i l e secret >=0 do
skip
end ; (*MH *)(*hc = H *)send 1 t o publicChannel
w h i l e secret >= 0 do
secret := secret - 1;
end ; (* T *)(*hc = L*)send 1 t o publicChannel
Andrew Bedford (Université Laval)

Prévention de fuites

Février 201516 / 20

Terminaison des boucles
Pour déterminer la terminaison des boucles, on utilise un oracle.

Andrew Bedford (Université Laval)

Prévention de fuites

Février 201517 / 20Démonstration

Andrew Bedford (Université Laval)

Prévention de fuites

Février 201518 / 20

Notre approche en bref :1

2
3

Vérifier avec notre système de type si le code contient des fuites
évidentes. Si c’est le cas, on rejette.
Sinon, le programme est instrumenté (de manière prouvée correct).
Le code est ensuite évalué partiellement.

Grâce à l’oracle et au niveau U, on accepte plus de programmes que
les autres approches similaires.
Le fait que l’on réécrit notre programme pour qu’il soit
non-interférent veut dire qu’il peut être optimisé.

Andrew Bedford (Université Laval)

Prévention de fuites

Février 201519 / 20

Questions ?

Andrew Bedford (Université Laval)

Prévention de fuites

Février 2015

20 / 20