HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Information Flow Security Certification for SPARK Programs

Abstract : SPARK 2014 (SPARK hereafter) is a programming language designed for building highly-reliable applications where safety and security are key requirements. SPARK platform performs a rigorous data/information flow analysis to ensure the safety and reliability of a program. However, the flow analysis is oriented towards establishing functional correctness and does not analyze for flow security of the program. Thus, there is a need to augment the analysis that would enable us to certify SPARK programs for security. In this paper, we propose an analysis to find information flow leaks in a SPARK program using a Dynamic Labelling (DL) approach for multi-level security (MLS) programs and describe an effective algorithm for detecting information leaks in SPARK programs, including classes of termination/progress-sensitive computations. Further, we illustrate the application of our approach for overcoming information leaks through unsanitized sensitive data. We also show how SPARK can be extended for realizing MLS systems that invariably need declassification through the illustration of an application of the method for security analysis of Needham-Schroeder public-key protocol.
Document type :
Conference papers
Complete list of metadata

Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, May 31, 2021 - 6:00:44 PM
Last modification on : Monday, May 31, 2021 - 6:08:46 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document


Distributed under a Creative Commons Attribution 4.0 International License



Sandip Ghosal, R. Shyamasundar. Information Flow Security Certification for SPARK Programs. 34th IFIP Annual Conference on Data and Applications Security and Privacy (DBSec), Jun 2020, Regensburg, Germany. pp.137-150, ⟨10.1007/978-3-030-49669-2_8⟩. ⟨hal-03243629⟩



Record views