The ACM SIGPLAN 7th Workshop on Programming Languages and Analysis for Security (PLAS) was held on June 15th, 2012 as a satellite event of PLDI 2012 in Beijing, China. The workshop featured six full papers and three position papers. The workshop also featured invited talks by Andrew Myers of Cornell University and Gilles Barthe of IMDEA Software.
Proceeding Downloads
Typing illegal information flows as program effects
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 ...
Knowledge-oriented secure multiparty computation
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 ...
Security-policy monitoring and enforcement with JavaMOP
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 ...
Security correctness for secure nested transactions: position paper
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 ...
A generic approach for security policies composition: position paper
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 ...
Static flow-sensitive & context-sensitive information-flow analysis for software product lines: position paper
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 ...
Towards a taint mode for cloud computing web applications
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 ...
Hash-flow taint analysis of higher-order programs
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 ...
Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment: a case study within the FoCaLiZe environment
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 ...