Qualitative and quantitative information flow analysis for multi-threaded programs

Minh Tri Ngo

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    191 Downloads (Pure)


    In today's information-based society, guaranteeing information security plays an important role in all aspects of life: communication between citizens and governments, military, companies, financial information systems, web-based services etc. With the increasing popularity of computer systems with multiple CPUs, and CPUs with multiple cores, applications implemented in a multi-threaded fashion - containing multiple activities that can be executed concurrently - are becoming the standard. However, there are many challenges related to how to keep private information processed by multi-threaded systems secure in the best way. Firstly, during the execution of a multi-threaded program, data behave in an unpredictable way; and thus, it is difficult to predict what an attacker is able to observe. Secondly, with the help of more powerful computing techniques, the attackers are more and more powerful. Most existing approaches are not sufficient to guarantee confidentiality for multi-threaded programs. The goal of this thesis is to propose more suitable and practically efficient methods to analyze information flow of multi-threaded programs. Firstly, we formalize two qualitative confidentiality properties: (1) for non-deterministic programs, where we do not take into account the probabilistic behavior of programs; and (2) for probabilistic programs, where we assume to have knowledge about the probability of scheduling events. We propose verification methods to verify these information flow properties. These techniques not only give precise and efficient verification of confidentiality properties, but also are relevant outside the security context. We also develop a tool which implements these techniques, and demonstrate its practical application on some case studies. Secondly, for programs that leak secret information, it is also interesting to know the quantity of information that has been revealed. We define and investigate quantitative security policies that offer a richer security policy than the traditional qualitative properties, since the amount of leakage can be used to decide whether we can tolerate the minor leakage. We propose two novel models of quantitative information flow analysis: (1) for a program where the attacker is able to influence the initial values of public data; and (2) for a program where the attacker is able to control the ordering of executed threads.
    Original languageEnglish
    Awarding Institution
    • University of Twente
    • van de Pol, Jaco , Supervisor
    • Huisman, Marieke, Supervisor
    Award date17 Apr 2014
    Place of PublicationEnschede
    Print ISBNs978-90-365-3652-3
    Publication statusPublished - 17 Apr 2014


    • IR-90497
    • METIS-303342


    Dive into the research topics of 'Qualitative and quantitative information flow analysis for multi-threaded programs'. Together they form a unique fingerprint.

    Cite this