Qualitative and quantitative information flow analysis for multi-threaded programs

Minh Tri Ngo

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

45 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 UTAcademic

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