Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA Methodology for Information Flow Experiments
232
0
0.0
(
0
)
Added by
Michael Tschantz
Publication date
2014
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Information flow analysis has largely ignored the setting where the analyst has neither control over nor a complete model of the analyzed system. We formalize such limited information flow analyses and study an instance of it: detecting the usage of data by websites. We prove that these problems are ones of causal inference. Leveraging this connection, we push beyond traditional information flow analysis to provide a systematic methodology based on experimental science and statistical analysis. Our methodology allows us to systematize prior works in the area viewing them as instances of a general approach. Our systematic study leads to practical advice for improving work on detecting data usage, a previously unformalized area. We illustrate these concepts with a series of experiments collecting data on the use of information by websites, which we statistically analyze.
rate research
Read More
We present a methodology for creating information flow specifications of hardware designs. Such specifications can help designers better understand their design and are necessary for security validation processes. By combining information flow tracking and specification mining, we are able to produce information flow properties of a design without prior knowledge of security agreements or specifications. We develop a tool, Isadora, to evaluate our methodology. We demonstrate Isadora may define the information flows within an access control module in isolation and within an SoC and over a RISC-V design. Over the access control module, Isadora mined output completely covers an assertion based security specification of the design provided by the designers. For both the access control module and RISC-V, we sample Isadora output properties and find 10 out of 10 and 8 out of 10 properties, respectively, define the design behavior to relevant to a Common Weakness Enumeration (CWE). We find our methodology may independently mine security properties manually developed by hardware designers, automatically generate properties describing CWEs over a design, and scale to SoC and CPU designs.
Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing program outputs. This approach is shown to elegantly capture standard notions of noninterference and declassification in the literature as well as information flow properties where sensitive and public data intermingle in delicate ways.
Noninterference offers a rigorous end-to-end guarantee for secure propagation of information. However, real-world systems almost always involve security requirements that change during program execution, making noninterference inapplicable. Prior works alleviate the limitation to some extent, but even for a veteran in information flow security, understanding the subtleties in the syntax and semantics of each policy is challenging, largely due to very different policy specification languages, and more fundamentally, semantic requirements of each policy. We take a top-down approach and present a novel information flow policy, called Dynamic Release, which allows information flow restrictions to downgrade and upgrade in arbitrary ways. Dynamic Release is formalized on a novel framework that, for the first time, allows us to compare and contrast various dynamic policies in the literature. We show that Dynamic Release generalizes declassification, erasure, delegation and revocation. Moreover, it is the only dynamic policy that is both applicable and correct on a benchmark of tests with dynamic policy.
Mobile and IoT applications have greatly enriched our daily life by providing convenient and intelligent services. However, these smart applications have been a prime target of adversaries for stealing sensitive data. It poses a crucial threat to users identity security, financial security, or even life security. Research communities and industries have proposed many Information Flow Control (IFC) techniques for data leakage detection and prevention, including secure modeling, type system, static analysis, dynamic analysis, textit{etc}. According to the applications development life cycle, although most attacks are conducted during the applications execution phase, data leakage vulnerabilities have been introduced since the design phase. With a focus on lifecycle protection, this survey reviews the recent representative works adopted in different phases. We propose an information flow based defensive chain, which provides a new framework to systematically understand various IFC techniques for data leakage detection and prevention in Mobile and IoT applications. In line with the phases of the application life cycle, each reviewed work is comprehensively studied in terms of technique, performance, and limitation. Research challenges and future directions are also pointed out by consideration of the integrity of the defensive chain.
Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, and channel capacity. This paper investigates the hardness and possibilities of precisely checking and inferring quantitative information flow according to such definitions. We prove that, even for just comparing two programs on which has the larger flow, none of the definitions is a k-safety property for any k, and therefore is not amenable to the self-composition technique that has been successfully applied to precisely checking non-interference. We also show a complexity theoretic gap with non-interference by proving that, for loop-free boolean programs whose non-interference is coNP-complete, the comparison problem is #P-hard for all of the definitions. For positive results, we show that universally quantifying the distribution in the comparison problem, that is, comparing two programs according to the entropy based definitions on which has the larger flow for all distributions, is a 2-safety problem in general and is coNP-complete when restricted for loop-free boolean programs. We prove this by showing that the problem is equivalent to a simple relation naturally expressing the fact that one program is more secure than the other. We prove that the relation also refines the channel-capacity based definition, and that it can be precisely checked via the self-composition as well as the interleaved self-composition technique.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
