An official website of the United States government
This paper considers a wireless network where multiple flows are delivering status updates about their respective information sources. An end user aims to make accurate real-time estimations about the status of each information source using its received packets. As the accuracy of estimation is most impacted by events in the recent past, we propose to measure the credibility of an information flow by the number of timely deliveries in a window of the recent past, and say that a flow suffers from a loss-of-credibility (LoC) if this number is insufficient for the end user to make an accurate estimation. We then study the problem of minimizing the system-wide LoC in wireless networks where each flow has different requirement and link quality. We show that the problem of minimizing the system-wide LoC requires the control of temporal variance of timely deliveries for each flow. This feature makes our problem significantly different from other optimization problems that only involves the average of control variables. Surprisingly, we show that there exists a simple online scheduling algorithm that is near-optimal. Simulation results show that our proposed algorithm is significantly better than other state-of-the-art policies.
more »
« less
This content will become publicly available on September 1, 2026
Gray-box runtime enforcement of hyperproperties
Abstract Enforcement of information-flow policies has been extensively studied by language-based approaches over the past few decades. In this paper, we propose an alternative, novel, general, and effective approach using enforcement ofhyperproperties– a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We studyblack-vs.gray-vs.white-boxenforcement of hyperproperties expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer has null, some, or complete information about the implementation of the system under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce the problem to controller synthesis for hyperproperties and subsequently to the satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers are transferable with low-overhead. We conduct a rich set of case studies, including information-flow control for JavaScript code, as well as synthesizing obfuscators for control plants.
more »
« less
- Award ID(s):
- 2245114
- PAR ID:
- 10629124
- Publisher / Repository:
- Springer
- Date Published:
- Journal Name:
- Acta Informatica
- Volume:
- 62
- Issue:
- 3
- ISSN:
- 0001-5903
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Scripts on webpages could steal sensitive user data. Much work has been done, both in modeling and implementation, to enforce information flow control (IFC) of webpages to mitigate such attacks. It is common to model scripts running in an IFC mechanism as a reactive program. However, this model does not account for dynamic script behavior such as user action simulation, new DOM element generation, or new event handler registration, which could leak information. In this paper, we investigate how to secure sensitive user information, while maintaining the flexibility of declassification, even in the presence of active attackers-those who can perform the aforementioned actions. Our approach extends prior work on secure-multi-execution with stateful declassification by treating script-generated content specially to ensure that declassification policies cannot be manipulated by them. We use a knowledge-based progress-insensitive definition of security and prove that our enforcement mechanism is sound. We further prove that our enforcement mechanism is precise and has robust declassification (i.e. active attackers cannot learn more than their passive counterpart).more » « less
-
Many high-level security requirements are about the allowed flow of information in programs, but are difficult to make precise because they involve selective downgrading. Quite a few mutually incompatible and ad-hoc approaches have been proposed for specifying and enforcing downgrading policies. Prior surveys of these approaches have not provided a unifying technical framework. Notions from epistemic logic have emerged as a good approach to policy semantics but are considerably removed from well developed static and dynamic enforcement techniques. We develop a unified framework for expressing, giving meaning and enforcing information downgrading policies that builds on commonly known and widely deployed concepts and techniques, especially static and dynamic assertion checking. These concepts should make information flow accessible and enable developers without special training to specify precise policies. The unified framework allows to directly compare different policy specification styles and enforce them by leveraging existing techniques.more » « less
-
This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enforcement library with the Yesod web programming framework. The implementation has two parts. First, we extract the core of LIO into a monad transformer (LMonad) and then apply it to Yesod’s core monad. Second, we extend Yesod’s table definition DSL and query functionality to permit defining and enforcing label-based policies on tables and enforcing them during query processing. LWeb’s policy language is expressive, permitting dynamic per-table and per-row policies. We formalize the essence of LWeb in the λLWebcalculus and mechanize the proof of noninterference in Liquid Haskell. This mechanization constitutes the first metatheoretic proof carried out in Liquid Haskell. We also used LWeb to build a substantial web site hosting the Build it, Break it, Fix it security-oriented programming contest. The site involves 40 data tables and sophisticated policies. Compared to manually checking security policies, LWeb imposes a modest runtime overhead of between 2% to 21%. It reduces the trusted code base from the whole application to just 1% of the application code, and 21% of the code overall (when counting LWeb too).more » « less
-
The increasing societal concern for consumer information privacy has led to the enforcement of privacy regulations worldwide. In an effort to adhere to privacy regulations such as the General Data Protection Regulation (GDPR), many companies’ privacy policies have become increasingly lengthy and complex. In this study, we adopted the computational design science paradigm to design a novel privacy policy evolution analytics framework to help identify how companies change and present their privacy policies based on privacy regulations. The framework includes a self-attentive annotation system (SAAS) that automatically annotates paragraph-length segments in privacy policies to help stakeholders identify data practices of interest for further investigation. We rigorously evaluated SAAS against state-of-the-art machine learning (ML) and deep learning (DL)-based methods on a well-established privacy policy dataset, OPP-115. SAAS outperformed conventional ML and DL models in terms of F1-score by statistically significant margins. We demonstrate the proposed framework’s practical utility with an in-depth case study of GDPR’s impact on Amazon’s privacy policies. The case study results indicate that Amazon’s post-GDPR privacy policy potentially violates a fundamental principle of GDPR by causing consumers to exert more effort to find information about first-party data collection. Given the increasing importance of consumer information privacy, the proposed framework has important implications for regulators and companies. We discuss several design principles followed by the SAAS that can help guide future design science-based e-commerce, health, and privacy research.more » « less
