publication . Conference object . 2019

Logic against ghosts

Hung, Chih-Cheng; Papadopoulos, George A.; Blanchard, Allan; Kosmatov, Nikolai; Loulergue, Frédéric;
Open Access
  • Published: 08 Apr 2019
  • Publisher: ACM
  • Country: France
Abstract
International audience; Modern verification projects continue to offer new challenges for formal verification. One of them is the linked list module of Contiki, a popular open-source operating system for the Internet of Things. It has a rich API and uses a particular list representation that make it different from the classical linked list implementations. Being widely used in the OS, the list module is critical for reliability and security. A recent work verified the list module using ghost arrays. This article reports on a new verification effort for this module. Realized in the Frama-C/Wp tool, the new approach relies on logic lists. A logic list provides a c...
Read more
Persistent Identifiers

doi: 10.1145/3297280.3297495

Subjects
free text keywords: linked lists, deductive verification, Frama-C, operating system, [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], Formal verification, Lemma (mathematics), Implementation, Linked list, Internet of Things, business.industry, business, Formal specification, Programming language, computer.software_genre, computer, Computer science
Related Organizations
View more
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
Communities
Rural Digital Europe
Download fromView all 8 versions
https://hal.inria.fr/hal-02100...
Conference object
Provider: UnpayWall
Hal-Diderot
Conference object . 2019
Provider: Hal-Diderot
HAL-CEA
Conference object . 2019
Provider: HAL-CEA
ZENODO
Conference object . 2019
Provider: ZENODO
View more
27 references, page 1 of 2

[1] Andrew W. Appel. 2011. Verified Software Toolchain. In Programming Languages and Systems (ESOP) (March 26-April 3) (LNCS), Gilles Barthe (Ed.), Vol. 6602. Springer, 1-17. https://doi.org/10.1007/978-3-642-19718-5_1

[2] Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37, 2, Article 7 (April 2015), 7:1-7:31 pages. https://doi.org/10.1145/2701415

[3] Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers . Cambridge University Press. [OpenAIRE]

[4] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. 2018. ACSL: ANSI/ISO C Specification Language. http://frama-c.com/acsl.html

[5] Y. Bertot and P. Castéran. 2004. Interactive Theorem Proving and Program Development. Springer. https://doi.org/10.1007/978-3-662-07964-5 [OpenAIRE]

[6] Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. 2018. Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. In Proc. of the 10th NASA Formal Methods Symposium (NFM 2018) (LNCS), Vol. 10811. Springer, 37-53.

[7] Jochen Burghardt and Jens Gerlach. 2018. ACSL by Example. https://github. com/fraunhoferfokus/acsl-by-example

[8] Ádám Darvas and Peter Müller. 2010. Proving Consistency and Completeness of Model Classes Using Theory Interpretation. In Proc. of the 13th International Conference on Fundamental Approaches to Software Engineering (FASE 2010) (LNCS), Vol. 6013. Springer, 218-232.

[9] Claire Dross and Yannick Moy. 2017. Auto-Active Proof of Red-Black Trees in SPARK. In NASA Formal Methods - 9th International Symposium, NFM 2017, Mofett Field, CA, USA, May 16-18, 2017, Proceedings . 68-83. https://doi.org/10. 1007/978-3-319-57288-8_5 [OpenAIRE]

[10] Adam Dunkels, Bjorn Gronvall, and Thiemo Voigt. 2004. Contiki - A Lightweight and Flexible Operating System for Tiny Networked Sensors. In LCN 2014. IEEE. [OpenAIRE]

[11] Jean-Christophe Filliâtre and Andrei Paskevich. [n. d.]. Why3 - Where Programs Meet Provers. In ESOP 2013.

[12] Christoph Gladisch and Shmuel Tyszberowicz. 2015. Specifying linked data structures in JML for combining formal verification and testing. Science of Computer Programming 107-108 (2015), 19 - 40. https://doi.org/10.1016/j.scico. 2015.02.005 [OpenAIRE]

[13] Paolo Herms, Claude Marché, and Benjamin Monate. 2012. A Certified Multiprover Verification Condition Generator. In Verified Software: Theories, Tools, Experiments (VSTTE) (January 28-29) (LNCS), Vol. 7152. Springer, 2-17. https: //doi.org/10.1007/978-3-642-27705-4

[14] Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Franck Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In Nasa Formal Methods (NFM) (LNCS). Springer-Verlag, Berlin Heidelberg, 41-55. https://doi.org/10.1007/978-3-642-20398-5_4 [OpenAIRE]

[15] Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2015. Frama-C: A software analysis perspective. Formal Asp. Comput. 27, 3 (2015), 573-609. http://frama-c.com

27 references, page 1 of 2
Related research
Abstract
International audience; Modern verification projects continue to offer new challenges for formal verification. One of them is the linked list module of Contiki, a popular open-source operating system for the Internet of Things. It has a rich API and uses a particular list representation that make it different from the classical linked list implementations. Being widely used in the OS, the list module is critical for reliability and security. A recent work verified the list module using ghost arrays. This article reports on a new verification effort for this module. Realized in the Frama-C/Wp tool, the new approach relies on logic lists. A logic list provides a c...
Read more
Persistent Identifiers

doi: 10.1145/3297280.3297495

Subjects
free text keywords: linked lists, deductive verification, Frama-C, operating system, [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], Formal verification, Lemma (mathematics), Implementation, Linked list, Internet of Things, business.industry, business, Formal specification, Programming language, computer.software_genre, computer, Computer science
Related Organizations
View more
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
Communities
Rural Digital Europe
Download fromView all 8 versions
https://hal.inria.fr/hal-02100...
Conference object
Provider: UnpayWall
Hal-Diderot
Conference object . 2019
Provider: Hal-Diderot
HAL-CEA
Conference object . 2019
Provider: HAL-CEA
ZENODO
Conference object . 2019
Provider: ZENODO
View more
27 references, page 1 of 2

[1] Andrew W. Appel. 2011. Verified Software Toolchain. In Programming Languages and Systems (ESOP) (March 26-April 3) (LNCS), Gilles Barthe (Ed.), Vol. 6602. Springer, 1-17. https://doi.org/10.1007/978-3-642-19718-5_1

[2] Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37, 2, Article 7 (April 2015), 7:1-7:31 pages. https://doi.org/10.1145/2701415

[3] Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers . Cambridge University Press. [OpenAIRE]

[4] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. 2018. ACSL: ANSI/ISO C Specification Language. http://frama-c.com/acsl.html

[5] Y. Bertot and P. Castéran. 2004. Interactive Theorem Proving and Program Development. Springer. https://doi.org/10.1007/978-3-662-07964-5 [OpenAIRE]

[6] Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. 2018. Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. In Proc. of the 10th NASA Formal Methods Symposium (NFM 2018) (LNCS), Vol. 10811. Springer, 37-53.

[7] Jochen Burghardt and Jens Gerlach. 2018. ACSL by Example. https://github. com/fraunhoferfokus/acsl-by-example

[8] Ádám Darvas and Peter Müller. 2010. Proving Consistency and Completeness of Model Classes Using Theory Interpretation. In Proc. of the 13th International Conference on Fundamental Approaches to Software Engineering (FASE 2010) (LNCS), Vol. 6013. Springer, 218-232.

[9] Claire Dross and Yannick Moy. 2017. Auto-Active Proof of Red-Black Trees in SPARK. In NASA Formal Methods - 9th International Symposium, NFM 2017, Mofett Field, CA, USA, May 16-18, 2017, Proceedings . 68-83. https://doi.org/10. 1007/978-3-319-57288-8_5 [OpenAIRE]

[10] Adam Dunkels, Bjorn Gronvall, and Thiemo Voigt. 2004. Contiki - A Lightweight and Flexible Operating System for Tiny Networked Sensors. In LCN 2014. IEEE. [OpenAIRE]

[11] Jean-Christophe Filliâtre and Andrei Paskevich. [n. d.]. Why3 - Where Programs Meet Provers. In ESOP 2013.

[12] Christoph Gladisch and Shmuel Tyszberowicz. 2015. Specifying linked data structures in JML for combining formal verification and testing. Science of Computer Programming 107-108 (2015), 19 - 40. https://doi.org/10.1016/j.scico. 2015.02.005 [OpenAIRE]

[13] Paolo Herms, Claude Marché, and Benjamin Monate. 2012. A Certified Multiprover Verification Condition Generator. In Verified Software: Theories, Tools, Experiments (VSTTE) (January 28-29) (LNCS), Vol. 7152. Springer, 2-17. https: //doi.org/10.1007/978-3-642-27705-4

[14] Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Franck Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In Nasa Formal Methods (NFM) (LNCS). Springer-Verlag, Berlin Heidelberg, 41-55. https://doi.org/10.1007/978-3-642-20398-5_4 [OpenAIRE]

[15] Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2015. Frama-C: A software analysis perspective. Formal Asp. Comput. 27, 3 (2015), 573-609. http://frama-c.com

27 references, page 1 of 2
Related research
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue