Formal analysis and offline monitoring of electronic exams

Ali Kassem 1, 2 Yliès Falcone 3 Pascal Lafourcade 4
2 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
3 CORSE - Compiler Optimization and Run-time Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : More and more universities are moving toward electronic exams (in short e-exams). This migration exposes exams to additional threats, which may come from the use of the information and communication technology. In this paper, we identify and define several security properties for e-exam systems. Then, we show how to use these properties in two complementary approaches: model-checking and monitoring. We illustrate the validity of our definitions by analyzing a real e-exam used at the pharmacy faculty of University Grenoble Alpes (UGA) to assess students. On the one hand, we instantiate our properties as queries for ProVerif, an automatic verifier of cryptographic protocols, and we use it to check our modeling of UGA exam specifications. ProVerif found some attacks. On the other hand, we express our properties as Quantified Event Automata (QEAs), and we synthesize them into monitors using MarQ, a Java tool designed to implement QEAs. Then, we use these monitors to verify real exam executions conducted by UGA. Our monitors found fraudulent students and discrepancies between the specifications of UGA exam and its implementation.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2017, 51 (1), pp.117 - 153. 〈10.1007/s10703-017-0280-0〉
Liste complète des métadonnées

Littérature citée [46 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01653884
Contributeur : Yliès Falcone <>
Soumis le : jeudi 14 décembre 2017 - 16:42:24
Dernière modification le : jeudi 11 janvier 2018 - 06:28:14

Fichier

fmsd6.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Ali Kassem, Yliès Falcone, Pascal Lafourcade. Formal analysis and offline monitoring of electronic exams. Formal Methods in System Design, Springer Verlag, 2017, 51 (1), pp.117 - 153. 〈10.1007/s10703-017-0280-0〉. 〈hal-01653884〉

Partager

Métriques

Consultations de la notice

99

Téléchargements de fichiers

12