Qualitative and quantitative information flow analysis for multi-threaded programs

Minh Tri Ngo

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    61 Downloads (Pure)

    Abstract

    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
    Supervisors/Advisors
    • van de Pol, Jaco , Supervisor
    • Huisman, Marieke , Supervisor
    Award date17 Apr 2014
    Place of PublicationEnschede
    Publisher
    Print ISBNs978-90-365-3652-3
    DOIs
    Publication statusPublished - 17 Apr 2014

    Fingerprint

    Program processors
    Security of data
    Information systems
    Computer systems
    Scheduling
    Communication
    Industry

    Keywords

    • IR-90497
    • METIS-303342

    Cite this

    Ngo, Minh Tri. / Qualitative and quantitative information flow analysis for multi-threaded programs. Enschede : Universiteit Twente, 2014. 180 p.
    @phdthesis{32d6db2111ab4c6a91fb7aea46fad265,
    title = "Qualitative and quantitative information flow analysis for multi-threaded programs",
    abstract = "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.",
    keywords = "IR-90497, METIS-303342",
    author = "Ngo, {Minh Tri}",
    year = "2014",
    month = "4",
    day = "17",
    doi = "10.3990/1.9789036536523",
    language = "English",
    isbn = "978-90-365-3652-3",
    series = "CTIT Ph.D. thesis series",
    publisher = "Universiteit Twente",
    number = "14-305",
    school = "University of Twente",

    }

    Qualitative and quantitative information flow analysis for multi-threaded programs. / Ngo, Minh Tri.

    Enschede : Universiteit Twente, 2014. 180 p.

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    TY - THES

    T1 - Qualitative and quantitative information flow analysis for multi-threaded programs

    AU - Ngo, Minh Tri

    PY - 2014/4/17

    Y1 - 2014/4/17

    N2 - 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.

    AB - 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.

    KW - IR-90497

    KW - METIS-303342

    U2 - 10.3990/1.9789036536523

    DO - 10.3990/1.9789036536523

    M3 - PhD Thesis - Research UT, graduation UT

    SN - 978-90-365-3652-3

    T3 - CTIT Ph.D. thesis series

    PB - Universiteit Twente

    CY - Enschede

    ER -

    Ngo MT. Qualitative and quantitative information flow analysis for multi-threaded programs. Enschede: Universiteit Twente, 2014. 180 p. (CTIT Ph.D. thesis series; 14-305). (IPA Dissertation series; 2014-05). https://doi.org/10.3990/1.9789036536523