publication . Conference object . Other literature type . Part of book or chapter of book . Article . 2018

Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C

Blanchard, Allan; Kosmatov, Nikolai; Loulergue, Frédéric;
Open Access
  • Published: 17 Apr 2018
  • Country: France
Abstract
International audience; Internet of Things (IoT) applications are becoming increasingly critical and require rigorous formal verification. In this paper we target Contiki, a widely used open-source OS for IoT, and present a verification case study of one of its most critical modules: that of linked lists. Its API and list representation differ from the classical linked list implementations, and are particularly challenging for deductive verification. The proposed verification technique relies on a parallel view of a list through a companion ghost array. This approach makes it possible to perform most proofs automatically using the Frama-C/WP tool, only a small n...
Subjects
free text keywords: linked lists, deductive verification, operating system, internet of things, Frama-C, internet of things, operating system, Frama-C, linked lists, deductive verification, [INFO.INFO-OS]Computer Science [cs]/Operating Systems [cs.OS], [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Proof assistant, Lemma (mathematics), Computer science, Mathematical proof, Internet of Things, business.industry, business, Formal verification, Linked list, Implementation, Programming language, computer.software_genre, computer
Funded by
EC| VESSEDIA
Project
VESSEDIA
VERIFICATION ENGINEERING OF SAFETY AND SECURITY CRITICAL DYNAMIC INDUSTRIAL APPLICATIONS
  • Funder: European Commission (EC)
  • Project Code: 731453
  • Funding stream: H2020 | RIA
Validated by funder
Communities
Rural Digital Europe

1. Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) Programming Languages and Systems (ESOP). LNCS, vol. 6602, pp. 1-17. Springer (2011)

2. Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37(2), 7:1-7:31 (Apr 2015)

3. Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge University Press (2014) [OpenAIRE]

4. Baudin, P., Cuoq, P., Filliaˆtre, J.C., Marche´, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, http://frama-c.com/acsl.html

5. Bertot, Y., Caste´ran, P.: Interactive Theorem Proving and Program Development. Springer (2004)

6. Blanchard, A., Kosmatov, N., Lemerre, M., Loulergue, F.: A case study on formal verification of the anaxagoros hypervisor paging system with Frama-C. In: Proc. of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015). LNCS, vol. 9128, pp. 15-30. Springer (Jun 2015) [OpenAIRE]

7. Brookes, S., O'Hearn, P.W.: Concurrent separation logic. ACM SIGLOG News 3(3), 47-65 (Aug 2016)

8. Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. SIGSOFT Softw. Eng. Notes 31(3), 25-37 (May 2006)

9. Dross, C., Moy, Y.: Auto-active proof of red-black trees in SPARK. In: NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. pp. 68-83 (2017) [OpenAIRE]

10. Dunkels, A., Gronvall, B., Voigt, T.: Contiki - a lightweight and flexible operating system for tiny networked sensors. In: LCN 2014. IEEE (2004)

Abstract
International audience; Internet of Things (IoT) applications are becoming increasingly critical and require rigorous formal verification. In this paper we target Contiki, a widely used open-source OS for IoT, and present a verification case study of one of its most critical modules: that of linked lists. Its API and list representation differ from the classical linked list implementations, and are particularly challenging for deductive verification. The proposed verification technique relies on a parallel view of a list through a companion ghost array. This approach makes it possible to perform most proofs automatically using the Frama-C/WP tool, only a small n...
Subjects
free text keywords: linked lists, deductive verification, operating system, internet of things, Frama-C, internet of things, operating system, Frama-C, linked lists, deductive verification, [INFO.INFO-OS]Computer Science [cs]/Operating Systems [cs.OS], [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Proof assistant, Lemma (mathematics), Computer science, Mathematical proof, Internet of Things, business.industry, business, Formal verification, Linked list, Implementation, Programming language, computer.software_genre, computer
Funded by
EC| VESSEDIA
Project
VESSEDIA
VERIFICATION ENGINEERING OF SAFETY AND SECURITY CRITICAL DYNAMIC INDUSTRIAL APPLICATIONS
  • Funder: European Commission (EC)
  • Project Code: 731453
  • Funding stream: H2020 | RIA
Validated by funder
Communities
Rural Digital Europe

1. Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) Programming Languages and Systems (ESOP). LNCS, vol. 6602, pp. 1-17. Springer (2011)

2. Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37(2), 7:1-7:31 (Apr 2015)

3. Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge University Press (2014) [OpenAIRE]

4. Baudin, P., Cuoq, P., Filliaˆtre, J.C., Marche´, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, http://frama-c.com/acsl.html

5. Bertot, Y., Caste´ran, P.: Interactive Theorem Proving and Program Development. Springer (2004)

6. Blanchard, A., Kosmatov, N., Lemerre, M., Loulergue, F.: A case study on formal verification of the anaxagoros hypervisor paging system with Frama-C. In: Proc. of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015). LNCS, vol. 9128, pp. 15-30. Springer (Jun 2015) [OpenAIRE]

7. Brookes, S., O'Hearn, P.W.: Concurrent separation logic. ACM SIGLOG News 3(3), 47-65 (Aug 2016)

8. Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. SIGSOFT Softw. Eng. Notes 31(3), 25-37 (May 2006)

9. Dross, C., Moy, Y.: Auto-active proof of red-black trees in SPARK. In: NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. pp. 68-83 (2017) [OpenAIRE]

10. Dunkels, A., Gronvall, B., Voigt, T.: Contiki - a lightweight and flexible operating system for tiny networked sensors. In: LCN 2014. IEEE (2004)

Any information missing or wrong?Report an Issue