NDLI: Merlin: specification inference for explicit information flow problems

Please wait, while we are loading the content...

Dynamic software updates: a VM-centric approach

Staged information flow for javascript

Lightweight annotations for controlling sharing in concurrent data structures

Progress guarantee for parallel programs via bounded lock-freedom

A decision procedure for subset constraints over regular languages

GC assertions: using the garbage collector to check heap properties

Sharing classes between families

Verified validation of lazy code motion

Automatic generation of library bindings using static analysis

A study of memory management for web-based applications on multicore processors

Programming model for a heterogeneous x86 platform

Safe and timely updates to multi-threaded programs

Laminar: practical fine-grained decentralized information flow control

A randomized dynamic program analysis technique for detecting real deadlocks

Stretching transactional memory

Verifiable composition of deterministic grammars

SoftBound: highly compatible and complete spatial memory safety for c

Typed self-representation

Proving optimizations correct using parameterized program equivalence

Snugglebug: a powerful approach to weakest preconditions

Efficiently and precisely locating memory leaks and bloat

Binary analysis for measurement and attribution of program performance

CEAL: a C-based language for self-adjusting computation

Merlin: specification inference for explicit information flow problems

FastTrack: efficient and precise dynamic race detection

Parallelizing sequential applications on commodity hardware using a low-cost software transactional memory

Analyzing recursive programs using a fixed-point calculus

Implementation of the memory-safe full ANSI-C compiler

Type-based data structure verification

An integrated proof language for imperative programs

Control-flow refinement and progress invariants for bound analysis

Chameleon: adaptive selection of collections

Semantics-aware trace analysis

PetaBricks: a language and compiler for algorithmic choice

TAJ: effective taint analysis of web applications

LiteRace: effective sampling for lightweight data-race detection

Towards a holistic approach to auto-parallelization: integrating profile-driven parallelism detection and machine-learning based mapping

Program verification using templates over predicate abstraction

Error propagation analysis for file systems

Go with the flow: profiling copies to find runtime bloat

Trace-based just-in-time type specialization for dynamic languages

Merlin: specification inference for explicit information flow problems

Content Provider	ACM Digital Library
Author	Nori, Aditya V. Rajamani, Sriram K. Livshits, Benjamin Banerjee, Anindya
Abstract	The last several years have seen a proliferation of static and runtime analysis tools for finding security violations that are caused by explicit information flow in programs. Much of this interest has been caused by the increase in the number of vulnerabilities such as cross-site scripting and SQL injection. In fact, these explicit information flow vulnerabilities commonly found in Web applications now outnumber vulnerabilities such as buffer overruns common in type-unsafe languages such as C and C++. Tools checking for these vulnerabilities require a specification to operate. In most cases the task of providing such a specification is delegated to the user. Moreover, the efficacy of these tools is only as good as the specification. Unfortunately, writing a comprehensive specification presents a major challenge: parts of the specification are easy to miss, leading to missed vulnerabilities; similarly, incorrect specifications may lead to false positives. This paper proposes Merlin, a new approach for automatically inferring explicit information flow specifications from program code. Such specifications greatly reduce manual labor, and enhance the quality of results, while using tools that check for security violations caused by explicit information flow. Beginning with a data propagation graph, which represents interprocedural flow of information in the program, Merlin aims to automatically infer an information flow specification. Merlin models information flow paths in the propagation graph using probabilistic constraints. A naive modeling requires an exponential number of constraints, one per path in the propagation graph. For scalability, we approximate these path constraints using constraints on chosen triples of nodes, resulting in a cubic number of constraints. We characterize this approximation as a probabilistic abstraction, using the theory of probabilistic refinement developed by McIver and Morgan. We solve the resulting system of probabilistic constraints using factor graphs, which are a well-known structure for performing probabilistic inference. We experimentally validate the Merlin approach by applying it to 10 large business-critical Web applications that have been analyzed with CAT.NET, a state-of-the-art static analysis tool for .NET. We find a total of 167 new confirmed specifications, which result in a total of 322 additional vulnerabilities across the 10 benchmarks. More accurate specifications also reduce the false positive rate: in our experiments, Merlin-inferred specifications result in 13 false positives being removed; this constitutes a 15% reduction in the CAT.NET false positive rate on these 10 programs. The final false positive rate for CAT.NET after applying Merlin in our experiments drops to under 1%.
Starting Page	75
Ending Page	86
Page Count	12
File Format	PDF
ISBN	9781605583921
DOI	10.1145/1542476.1542485
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2009-06-15
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Security analysis tools Specification inference
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Merlin: Specification Inference for Explicit Information Flow Problems

Merlin: specification inference for explicit information flow problems.

Merlin: Specification Inference for Explicit Information Flow Problems

Merlin: Specification Inference for Explicit Information Flow Problems

Merlin:specification inference for explicit information flow problems

Static analysis for inference of explicit information flow

Modelgen: mining explicit information flow specifications from concrete executions

Static Information Flow Analysis with Handling of Implicit Flows and a Study on Effects of Implicit Flows vs Explicit Flows

Efficient type inference for secure information flow

Merlin: specification inference for explicit information flow problems

Similar Documents

Merlin: Specification Inference for Explicit Information Flow Problems

Merlin: specification inference for explicit information flow problems.

Merlin: Specification Inference for Explicit Information Flow Problems

Merlin: Specification Inference for Explicit Information Flow Problems

Merlin:specification inference for explicit information flow problems

Static analysis for inference of explicit information flow

Modelgen: mining explicit information flow specifications from concrete executions

Static Information Flow Analysis with Handling of Implicit Flows and a Study on Effects of Implicit Flows vs Explicit Flows

Efficient type inference for secure information flow

Merlin: specification inference for explicit information flow problems