PLDI

Specification of information flow policies is classically based on a security labeling and a lattice of security levels that establishes how information can flow between security levels. We present a type and effect system for determining the least ...

Protocols for secure multiparty computation (SMC) allow a set of mutually distrusting parties to compute a function f of their private inputs while revealing nothing about their inputs beyond what is implied by the result. Depending on f, however, the ...

Software security attacks represent an ever growing problem. One way to make software more secure is to use Inlined Reference Monitors (IRMs), which allow security specifications to be inlined inside a target program to ensure its compliance with the ...

This article considers the synthesis of two long-standing lines of research in computer security: security correctness for multilevel databases, and language-based security. The motivation is an approach to supporting end-to-end security for a wide ...

When modelling access control in distributed systems, the problem of security policies composition arises. Much work has been done on different ways of combining policies, and using different logics to do this. In this paper, we propose a more general ...

A software product line encodes a potentially large variety of software products as variants of some common code base, e.g., through the use of #ifdef statements or other forms of conditional compilation. Traditional information-flow analyses cannot ...

Cloud computing is generally understood as the distribution of data and computations over the Internet. Over the past years, there has been a steep increase in web sites using this technology. Unfortunately, those web sites are not exempted from ...

As web applications have grown in popularity, so have attacks on such applications. Cross-site scripting and injection attacks have become particularly problematic. Both vulnerabilities stem, at their core, from improper sanitization of user input.

We ...

FoCaLiZe is an object-oriented programming environment that combines specifications, programs and proofs in the same language. This paper describes how its features can be used to formally express specifications and to develop by stepwise refinement the ...