Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userLiquid Information Flow Control
58
0
0.0
(
0
)
Added by
Nadia Polikarpova
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, thereby easing the programmer burden of implementing policy enforcing code throughout the application. The main insight behind Lifty is to encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking of complex, data dependent policies, and power our repair mechanism via type-driven error localization and patch synthesis. Our experience using Lifty to implement three case studies from the literature shows that (1) the Lifty policy language is sufficiently expressive to specify many real-world policies, (2) the Lifty type checker is able to verify secure programs and find leaks in insecure programs quickly, and (3) even if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time.
rate research
Read More
Safely integrating third-party code in applications while protecting the confidentiality of information is a long-standing problem. Pure functional programming languages, like Haskell, make it possible to enforce lightweight information-flow control through libraries like MAC by Russo. This work presents DepSec, a MAC inspired, dependently typed library for static information-flow control in Idris. We showcase how adding dependent types increases the expressiveness of state-of-the-art static information-flow control libraries and how DepSec matches a special-purpose dependent information-flow type system on a key example. Finally, we show novel and powerful means of specifying statically enforced declassification policies using dependent types.
Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it requires reasoning on these phases separately. In this paper we discuss techniques for proving termination of such programs, in particular: (1) using multiphase ranking functions, where we will discuss theoretical aspects of such ranking functions for several kinds of program representations; and (2) using control-flow refinement, in particular partial evaluation of Constrained Horn Clauses, to simplify the control-flow allowing, among other things, to prove termination with simpler ranking functions.
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 Yesods core monad. Second, we extend Yesods table definition DSL and query functionality to permit defining and enforcing label-based policies on tables and enforcing them during query processing. LWebs policy language is expressive, permitting dynamic per-table and per-row policies. We formalize the essence of LWeb in the $lambda_{LWeb}$ calculus 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).
We initiate the study of Access Control Encryption (ACE), a novel cryptographic primitive that allows fine-grained access control, by giving different rights to different users not only in terms of which messages they are allowed to receive, but also which messages they are allowed to send. Classical examples of security policies for information flow are the well known Bell-Lapadula [BL73] or Biba [Bib75] model: in a nutshell, the Bell-Lapadula model assigns roles to every user in the system (e.g., public, secret and top-secret). A users role specifies which messages the user is allowed to receive (i.e., the no read-up rule, meaning that users with public clearance should not be able to read messages marked as secret or top-secret) but also which messages the user is allowed to send (i.e., the no write-down rule, meaning that a user with top-secret clearance should not be able to write messages marked as secret or public). To the best of our knowledge, no existing cryptographic primitive allows for even this simple form of access control, since no existing cryptographic primitive enforces any restriction on what kind of messages one should be able to encrypt. Our contributions are: - Introducing and formally defining access control encryption (ACE); - A construction of ACE with complexity linear in the number of the roles based on classic number theoretic assumptions (DDH, Paillier); - A construction of ACE with complexity polylogarithmic in the number of roles based on recent results on cryptographic obfuscation;
The optimally designed control of quantum systems is playing an increasingly important role to engineer novel and more efficient quantum technologies. Here, in the scenario represented by controlling an arbitrary quantum system via the interaction with an another optimally initialized auxiliary quantum system, we show that the quantum channel capacity sets the scaling behaviour of the optimal control error. Specifically, we prove that the minimum control error is ensured by maximizing the quantum capacity of the channel mapping the initial control state into the target state of the controlled system, i.e., optimizing the quantum information flow from the controller to the system to be controlled. Analytical results, supported by numerical evidences, are provided when the systems and the controller are either qubits or single Bosonic modes and can be applied to a very large class of platforms for controllable quantum devices.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
