Formal Analysis of Security Guidelines for Program Certification

Organisation:	EURECOM Sophia-Antipolis (FRANCE) University of Nice (FRANCE) Telecom ParisTech
Functionality:	Formal Analysis of Security Guidelines for Program Certification
Tools used:	CADP (Construction and Analysis of Distributed Processes) JOANA (Java Object-sensitive ANAlysis)
Period:	2017
Description:	A widespread approach to establish a set of security objectives is to show that the developers have adhered to a set of security guidelines, such as OWASP or the CERT Coding Standard for Java. The authors propose to formalize the security guidelines by specifiying them as MCL formulae, and propose a framework combining program analysis and model checking to automate systematic verification of the security guidelines. The formal specification of the guidelines as MCL formulae is based on an analysis of the frequently encountered recommendations. Because these guidelines are typically dealing with data parameters, the data-handling capabilities of MCL are crucial. Most of the studied guidelines could be expressed as usual safety properties, encoded in MCL as "[R] false" (stating the absence of bad execution sequences characterized by R), or as basic liveness properties, encoded in MCL as "<R> true" (stating the existence of good execution sequences characterized by R). A catalog of patterns facilitates the formalization. The proposed framework has two principal parts: the model construction and the automatic verification. The former is based on an extension of JOANA tool, and produces a PDG (Program Dependency Graph), an abstract representation of the explicit and implicit dependencies of the program, annotated with labels to match those of the MCL formulas. From the PDG, the framework extracts a pLTS (parameterized Labelled Transition System). It is important to note that the annotated PDG and the pLTS are isomorphic, in the sense that both graphs have the same number of edges and the same number of nodes. Finally, the MCL formulae encoding the security guidelines are checked using EVALUATOR. In the case a property is not satisfied, the counter-example provided by EVALUATOR is reported back to the developer.
Conclusions:	MCL is appropriate to formally specify security guidelines, in particular thanks to its data-handling capabilities and the possibility to define patterns. EVALUATOR was integrated into a framework automating the verification of security guidelines, giving helpful feedback to developers if a guideline is not repsected.
Publications:	[Zhioua-Roudier-AmeurBoulifa-17-a] Zeineb Zhioua, Yves Roudier, and Rabéa Ameur-Boulifa. "Formal Specification and Verification of Security Guidelines". Proceedings of the 22nd Pacific Rim International Symposium on Dependable Computing (PRDC), Christchurch, Canterbury, New Zealand, IEEE, January 2017. Available on-line at: https://doi.org/10.1109/PRDC.2017.51 [Zhioua-Roudier-AmeurBoulifa-et-al-17] Zeineb Zhioua, Yves Roudier, Rabéa Ameur-Boulifa, Takoua Kechiche, and Stuart Short. "Tracking dependent information flows". Proceedings of the 3rd International Conference on Information Systems Security and Privacy (ICISSP 2017), Porto, Portugal, SciTePress, February 2017. Available on-line at: https://doi.org/10.5220/0006209301790189 or from the CADP Web site in PDF or PostScript [Zhioua-Roudier-AmeurBoulifa-17-b] Zeineb Zhioua, Yves Roudier, and Rabéa Ameur-Boulifa. "Formal Specification of Security Guidelines for Program Certification". Proceedings of the 11th International Symposium on Theoretical Aspects of Software Engineering (TASE 2017), Sophia-Antipolis, France, IEEE, September 2017. Available on-line at: https://doi.org/10.1109/TASE.2017.8285634 or from the CADP Web site in PDF or PostScript [Zhioua-AmeurBoulifa-Roudier-18] Zeineb Zhioua, Rabéa Ameur-Boulifa, and Yves Roudier. "Framework for the Formal Specification and Verification of Security Guidelines". Advances in Science, Technology and Engineering Systems Journal, volume 3, number 1, pages 38-48, January 2018. Available on-line at: http://dx.doi.org/10.25046/aj030106
Contact:	Rabéa Ameur-Boulifa Eurecom - Télécom ParisTech Soc Email: Rabea.Ameur-Boulifa at telecom-paristech.fr Tel: +33 (0)4 93 00 84 01 Fax: +33 (0)4 93 00 82 00
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page