nach oben

Formal Methods in System Design

Erschienen in:

01.06.2017

Formal analysis and offline monitoring of electronic exams

verfasst von: Ali Kassem, Yliès Falcone, Pascal Lafourcade

Erschienen in: Formal Methods in System Design | Ausgabe 1/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Monitorability for the Hennessy–Milner logic with recursion

Nächster Artikel Predictive runtime enforcement

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

www.side-sante.org.

http://www.proctoru.com.

https://github.com/selig/qea.

Abadi M, Blanchet B (2005) Analyzing security protocols with secrecy types and logic programs. J ACM 52(1):102–146MathSciNetCrossRefMATH

Abadi M, Blanchet B, Comon-Lundh H (2009) Models and proofs of protocol security: a progress report. In: Bouajjani A, Maler O (eds) Computer aided verification, 21st international conference, CAV 2009, Grenoble, France, June 26–July 2, 2009. Proceedings, vol 5643 of lecture notes in computer science. Springer, Berlin, pp 35–49

Abadi M, Fournet C (2001) Mobile values, new names, and secure communication. In: Hankin C, Schmidt D (eds) Conference record of POPL 2001: the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages, London, UK, Jan 17–19, 2001, ACM, pp 104–115

Allamigeon X, Blanchet B (2005) Reconstruction of attacks against cryptographic protocols. In: 18th IEEE Computer Security Foundations Workshop, (CSFW-18 2005), 20–22 June 2005, Aix-en-Provence, France, pp 140–154. IEEE Computer Society

Arapinis M, Bursuc S, Ryan M (2012) Privacy supporting cloud computing: confichair, a case study. In: Degano P, Guttman JD (ed) Principles of security and trust-first international conference, POST 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24–April 1, 2012, proceedings, vol 7215 of lecture notes in computer science. Springer, Berlin, pp 89–108

Armando A, Basin DA, Boichut Y, Chevalier Y, Compagna L, Cuéllar J, Drielsma PH, Héam P-C, Kouchnarenko O, Mantovani J, Mödersheim S, von Oheimb D, Rusinowitch M, Santiago J, Turuani M, Viganò L, Vigneron L (2005) The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami K, Rajamani SK (eds) Computer aided verification, 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005, proceedings, vol 3576 of lecture notes in computer science. Springer, Berlin, pp 281–285

Backes M, Hritcu C, Maffei M (2008) Automated verification of remote electronic voting protocols in the applied pi-calculus. In: Proceedings of the 2008 21st IEEE computer security foundations symposium, CSF ’08, Washington, DC, USA, 2008. IEEE Computer Society, pp 195–209

Barringer H, Falcone Y, Havelund K, Reger G, Rydeheard DE, Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou D, Dominique M [45], pp 68–84

Bartocci E, Bonakdarpour B, Falcone Y (2014) First international competition on software for runtime verification. In: Bonakdarpour B, Smolka SA (ed) Runtime verification-5th international conference, RV 2014, Toronto, ON, Canada, Sept 22–25, 2014. Proceedings, vol 8734 of lecture notes in computer science. Springer, Berlin, pp 1–9

10.

Bartocci E, Falcone Y, Bonakdarpour B, Colombo C, Decker N, Havelund K, Joshi Y, Klaedtke F, Milewicz R, Reger G, Rosu G, Signoles J, Thoma D, Zalinescu E and Zhang Y (2017) First international competition on runtime verification: rules, benchmarks, tools, and final results of CRV 2014. Int J Softw Tools Technol Transf 19(2):1–40

11.

Bartocci E, Majumdar R (eds) (2015) Runtime verification—6th international conference, RV 2015 Vienna, Austria, Sept 22–25, 2015. Proceedings, vol 9333 of lecture notes in computer science. Springer, Berlin

12.

Basagiannis S, Katsaros P, Pombortsis A (2011) Synthesis of attack actions using model checking for the verification of security protocols. Secur Commun Netw 4(2):147–161CrossRef

13.

Basagiannis S, Katsaros P, Pombortsis A (2007) Intrusion attack tactics for the model checking of e-commerce security guarantees. In: Saglietti F, Oster N (eds) Computer safety, reliability, and security, 26th international conference, SAFECOMP 2007, Nuremberg, Germany, Sept 18–21, 2007, vol 4680 of lecture notes in computer science. Springer, Berlin, pp 238–251

14.

Basin D, Caronni G, Ereth S, Harvan M, Klaedtke F, Mantel H (2014) Scalable offline monitoring. In: Bonakdarpour B, Smolka SA (ed) Runtime verification: 5th international conference, RV 2014, Toronto, ON, Canada, Sept 22–25, 2014. Proceedings, Cham, 2014. Springer, Berlin, pp. 31–47

15.

Bauer AK, Falcone Y (2012) Decentralised LTL monitoring. In: Giannakopoulou D, Méry D (eds) Proceedings of the FM 2012: formal methods–18th international symposium, Paris, France, August 27–31, 2012. Lecture notes in computer science, vol 7436. Springer, New York, pp 85–100

16.

Bella G, Giustolisi R, Lenzini G, Ryan PYA (2015) A secure exam protocol without trusted parties. In: Federrath H, Gollmann D (eds) ICT systems security and privacy protection—30th IFIP TC 11 international conference, SEC 2015, Hamburg, Germany, May 26–28, 2015, Proceedings, vol 455 of IFIP Advances in Information and Communication Technology. Springer, Berlin, pp 495–509

17.

Blanchet B (2001) An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of the 14th IEEE workshop on computer security foundations, CSFW ’01, p 82, Washington, DC, USA, 2001. IEEE Computer Society

18.

Blanchet B (2002) From secrecy to authenticity in security protocols. In: Hermenegildo MV, Puebla G (eds) Static analysis, 9th international symposium, SAS 2002, Madrid, Spain, Sept 17–20, 2002, proceedings, vol 2477 of lecture notes in computer science. Springer, Berlin, pp 342–359

19.

Blanchet B (2013) Automatic verification of security protocols in the symbolic model: the verifier proverif. In: Aldini A, Lopez J, Martinelli F (eds) Foundations of security analysis and design VII—FOSAD 2012/2013 tutorial lectures, vol 8604 of Lecture Notes in Computer Science. Springer, Berlin, pp 54–87

20.

Blanchet B, Smyth B, Cheval V (2016) ProVerif 1.90: automatic cryptographic protocol verifier, user manual and tutorial, 2016. Originally appeared as Bruno B, Smyth B (2011) ProVerif 1.85: automatic cryptographic protocol verifier, user manual and tutorial

21.

Chadha R, Ciobâcă Ş, Kremer S (2012) Automated verification of equivalence properties of cryptographic protocols. In: Seidl H (ed) Programming languages and systems—21st European symposium on programming, ESOP 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24–April 1, 2012. Proceedings, vol 7211 of Lecture Notes in Computer Science. Springer, Berlin, pp 108–127

22.

Colombo C, Pace GJ (2013) Fast-forward runtime monitoring: an industrial case study. In: Qadeer S, Tasiran S (eds) Runtime verification: third international conference, RV 2012, Istanbul, Turkey, Sept 25–28, 2012, Revised Selected Papers. pp 214–228, Springer, Heidelberg

23.

Copeland L (2013) School cheating scandal shakes up atlanta. USA TODAY, April 2013. http://www.usatoday.com/story/news/nation/2013/04/13/atlanta-school-cheatring-race/2079327/

24.

Cortier V, Kremer S (2016) Formal models for analyzing security protocols: some lecture notes. In: Esparza J, Grumberg O, Sickert S. (eds) Dependable software systems engineering, vol 45 of NATO Science for Peace and Security Series D: Information and Communication Security. IOS Press, pp 33–58

25.

Cremers CJF (2008) The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta A, Malik S (eds) Computer aided verification, 20th international conference, CAV 2008, Princeton, NJ, USA, July 7–14, 2008, proceedings, vol 5123 of lecture notes in computer science. Springer, Berlin, pp 414–418

26.

Cremers CJF (2008) Unbounded verification, falsification, and characterization of security protocols by pattern refinement. In: Ning P, Syverson PF and Jha S (eds) Proceedings of the 2008 ACM conference on computer and communications security, CCS 2008, Alexandria, Virginia, USA, Oct 27–31, 2008. ACM, pp 119–128

27.

Cremers CJF, Lafourcade P, Nadeau P (2009) Comparing state spaces in automatic security protocol analysis. In: Cortier V, Kirchner C, Okada M, Sakurada H (eds) Formal to practical security—papers issued from the 2005–2008 French-Japanese collaboration, vol 5458 of lecture notes in computer science. Springer, Berlin, pp 70–94

28.

Dolev D, Yao A (1983) On the security of public key protocols. IEEE Trans Inf Theory 29(2):198–208MathSciNetCrossRefMATH

29.

Donzé A (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili T, Cook B, Jackson P (eds) Computer aided verification, 22nd international conference, CAV 2010, Edinburgh, UK, July 15–19, 2010. Proceedings, vol 6174 of lecture notes in computer science. Springer, Berlin, pp 167–170

30.

Dreier J, Giustolisi R, Kassem A, Lafourcade P, Lenzini G (2015) A framework for analyzing verifiability in traditional and electronic exams. In: Lopez J, Wu Y (eds) Information security practice and experience—11th international conference, ISPEC 2015, Beijing, China, May 5–8, 2015. Proceedings, vol 9065 of lecture notes in computer science. Springer, Berlin, pp 514–529

31.

Dreier J, Giustolisi R, Kassem A, Lafourcade P, Lenzini G, Ryan PYA (2014) Formal analysis of electronic exams. In: Obaidat MS, Holzinger A, Samarati P (eds) SECRYPT 2014—proceedings of the 11th international conference on security and cryptography, Vienna, Austria, 28–30 Aug, 2014. SciTePress, pp 101–112

32.

Dreier J, Giustolisi R, Kassem A, Lafourcade P, Lenzini G, Ryan PYA (2014) Formal security analysis of traditional and electronic exams. In: Obaidat MS, Holzinger A, Filipe J (eds) E-business and telecommunications—11th international joint conference, ICETE 2014, Vienna, Austria, Aug 28–30, 2014, Revised Selected Papers, vol 554 of Communications in Computer and Information Science, Springer, Berlin, pp 294–318

33.

Dreier J, Jonker H, Lafourcade P (2013) Defining verifiability in e-auction protocols. In: Chen K, Xie Q, Qiu W, Li N, Tzeng W-G (eds) 8th ACM symposium on information, computer and communications security, ASIA CCS ’13, Hangzhou, China—May 08–10, 2013, ACM, pp 547–552

34.

Dreier J, Kassem A, Lafourcade P (2015) Automated verification of e-cash protocols. In: E-business and telecommunications—12th international joint conference, ICETE 2015, Colmar, France, July 2022, 2015, Revised Selected Papers, pp 223–244

35.

Dreier J, Kassem A, Lafourcade P (2015) Formal analysis of e-cash protocols. In: Obaidat MS, Lorenz P, Samarati P (eds) SECRYPT 2015—proceedings of the 12th international conference on security and cryptography, Colmar, Alsace, France, 20–22 July, 2015. SciTePress, pp 65–75

36.

Falcone Y (2010) You should better enforce than verify. In: Barringer H, Falcone Y, Finkbeiner B, Havelund K, Lee I, Pace GJ, Rosu G, Sokolsky O, Tillmann N (eds) Runtime verification—first international conference, RV 2010, St. Julians, Malta, Nov 1–4, 2010. Proceedings, vol 6418 of lecture notes in computer science. Springer, Berlin, pp 89–105

37.

Falcone Y, Fernandez J-C, Jéron T, Marchand H, Mounier L (2012) More testable properties. STTT 14(4):407–437CrossRef

38.

Falcone Y, Fernandez J-C, Mounier L (2012) What can you verify and enforce at runtime? STTT 14(3):349–382CrossRef

39.

Falcone Y, Fernandez J-C, Mounier L (2009) Runtime verification of safety-progress properties. In: Bensalem S, Peled DA (eds) Runtime verification, 9th international workshop, RV 2009, Grenoble, France, June 26–28, 2009. Selected papers, vol 5779 of lecture notes in computer science. Springer, Berlin, pp 40–59

40.

Falcone Y, Havelund K, Reger G (2013) A tutorial on runtime verification. In: Broy M, Peled DA, Kalus G (eds) Engineering dependable software systems, vol 34 of NATO science for peace and security series, D: information and communication security. IOS Press, pp 141–175

41.

Falcone Y, Nickovic D, Reger G, Thoma D (2015) Second international competition on runtime verification CRV 2015. In: Bartocci E, Majumdar R [11], pp 405–422

42.

Figaro. Etudiants: les examens sur tablettes numériques appellés à se multiplier. Press release, Jan 2015. goo.gl/ahxQJD

43.

Foley SN, Jacob JL (1995) Specifying security for computer supported collaborative working. J Comput Secur 3(4):233–254CrossRef

44.

Francalanza A, Aceto L, Ingólfsdóttir A, On verifying hennessy-milner logic with recursion at runtime. In: Bartocci E, Majumdar R [11], pp 71–86

45.

Giannakopoulou D, Dominique M (eds) (2012) FM 2012: formal methods—18th international symposium, Paris, France, Aug 27–31, 2012. Proceedings, vol 7436 of lecture notes in computer science. Springer, Berlin

46.

Havelund K (2015) Rule-based runtime verification revisited. Int J Softw Tools Technol Transf 17(2):143–170CrossRef

47.

Havelund K, Goldberg A (2005) Verify your runs. In: Meyer B, Woodcock J (eds) Verified software: theories, tools, experiments, first IFIP TC 2/WG 2.3 conference, VSTTE 2005, Zurich, Switzerland, Oct 10–13, 2005, revised selected papers and discussions, vol 4171 of lecture notes in computer science. Springer, Berlin, pp 374–383

48.

Jin D, Meredith PON, Lee C, Rosu G (2012) Javamop: efficient parametric runtime monitoring framework. In: Glinz M, Murphy GC and Pezzè M (eds) 34th International conference on software engineering, ICSE 2012, June 2–9, 2012, Zurich, Switzerland. IEEE, pp 1427–1430

49.

Kassem A, Falcone Y, Lafourcade P (2015) Monitoring electronic exams. In: Bartocci E, Majumdar R (eds) Runtime verification—6th international conference, RV 2015 Vienna, Austria, Sept 22–25, 2015. Proceedings, vol 9333 of lecture notes in computer science. Springer, Berlin, pp 118–135

50.

Kassem A, Lafourcade P, Lakhnech Y (2014) Formal verification of e-reputation protocols. In: Cuppens F, García-Alfaro J, Heywood NZ, Fong PWL (eds) Foundations and practice of security—7th international symposium, FPS 2014, Montreal, QC, Canada, Nov 3–5, 2014. Revised selected papers, vol 8930 of lecture notes in computer science. Springer, Berlin, pp 247–261

51.

Katsaros P (2009) A roadmap to electronic payment transaction guarantees and a colored petri net model checking approach. Inf Softw Technol 51(2):235–257MathSciNetCrossRef

52.

Kim M, Kannan S, Lee I, Sokolsky O, Viswanathan M (2002) Computational analysis of run-time monitoring: fundamentals of java-mac. Electron Notes Theor Comput Sci 70(4):80–94CrossRef

53.

Kremer S, Ryan M, Smyth B (2010) Election verifiability in electronic voting protocols. In: Gritzalis D, Preneel B, Theoharidou M (eds) Computer security – ESORICS 2010: 15th European symposium on research in computer security, Athens, Greece, Sept 20–22, 2010. Proceedings, Springer, Berlin, pp 389–404

54.

Lafourcade P, Puys M (2015) Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties. In: García-Alfaro J, Kranakis E, Bonfante G (eds) Foundations and practice of security—8th international symposium, FPS 2015, Clermont-Ferrand, France, Oct 26–28, 2015, revised selected papers, vol 9482 of lecture notes in computer science. Springer, Berlin, pp 137–155

55.

Lafourcade P, Terrade V, Vigier S (2009) Comparison of cryptographic verification tools dealing with algebraic properties. In: Guttman J, Degano P (eds) Sixth international workshop on formal aspects in security and trust, (FAST’09). Eindhoven, Netherlands

56.

Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebr Program 78(5):293–303CrossRefMATH

57.

Meier S, Schmidt B, Cremers C, Basin DA (2013) The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina N, Veith H (eds) Computer aided verification—25th international conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, vol 8044 of lecture notes in computer science. Springer, Berlin, pp 696–701

58.

Navabpour S, Joshi Y, Wu CWW, Berkovich S, Medhat R, Bonakdarpour B, Fischmeister S (2013) Rithm: a tool for enabling time-triggered runtime verification for C programs. In: Meyer B, Baresi L, Mezini M (eds) Joint meeting of the european software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering, ESEC/FSE’13, Saint Petersburg, Russian Federation, Aug 18–26, 2013, ACM, pp 603–606

59.

Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: Misra J, Nipkow T, Sekerinski E (eds) FM 2006: formal methods, 14th international symposium on formal methods, Hamilton, Canada, Aug 21–27, 2006, proceedings, vol 4085 of lecture notes in computer science, Springer, Berlin, pp 573–586

60.

Ray S (2010) Scalable techniques for formal verification. Springer, BerlinCrossRefMATH

61.

Reger G (2014) Automata based monitoring and mining of execution traces. Ph.D. thesis, University of Manchester

62.

Reger G, Cruz HC, Rydeheard D (2015) Marq: monitoring at runtime with QEA. In: Baier C, Tinelli C (eds) Tools and algorithms for the construction and analysis of systems: 21st international conference, TACAS 2015, held as part of the european joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015, proceedings. Springer, Berlin, pp 596–610

63.

Reger G, Hallé S, Falcone Y (2016) Third international competition on runtime verification—CRV 2016. In: Falcone Y, Sánchez C (eds) Runtime verification—16th international conference, RV 2016, Madrid, Spain, Sept 23–30, 2016, proceedings, vol 10012 of lecture notes in computer science. Springer, Berlin, pp 21–37

64.

Schmidt B, Meier S, Cremers CJF, Basin DA (2012) Automated analysis of Diffie–Hellman protocols and advanced security properties. In: Chong S (ed) 25th IEEE computer security foundations symposium, CSF 2012, Cambridge, MA, USA, June 25–27, 2012. IEEE, pp 78–94

65.

Watson R (2014) Student visa system fraud exposed in BBC investigation. http://www.bbc.com/news/uk-26024375

Titel: Formal analysis and offline monitoring of electronic exams
verfasst von: Ali Kassem
Yliès Falcone
Pascal Lafourcade
Publikationsdatum: 01.06.2017
Verlag: Springer US
Erschienen in: Formal Methods in System Design / Ausgabe 1/2017
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-017-0280-0

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2017

Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles

Predictive runtime enforcement

R2U2: monitoring and diagnosis of security threats for unmanned aerial systems

Introduction to the special issue on runtime verification

Monitorability for the Hennessy–Milner logic with recursion

Robust online monitoring of signal temporal logic