Program Analysis for Information-flow security

Information-flow violations occur every time secret information is revealed to unauthorized entities without having been previously declassified (a violation of confidentiality), or untrusted data is used in security-sensitive computations without having been previously endorsed (a violation of integrity). As part of the LaBaSec project, we have designed and developed two static-analysis tools that help in the detection of information-flow violations in Web applications and component-based systems:

1. Taint Analysis for Java (TAJ) is a static-analysis tool that automatically detects integrity violations in Web applications. The TAJ algorithm was published in the proceedings of the PLDI 2009 conference. The TAJ technology that we have developed has been included in a product, IBM Rational AppScan Developer Edition (AppScan DE).

2. Mandatory Access Rights Certification of Objects (MARCO) is a static-analysis tool that can be used to automatically detect which portions of library code can be safely made "privilege-asserting". A block of library code is said to be privilege-asserting if it extends its own rights to its callers. If not inserted correctly, privilege-asserting code can easily lead to integrity violations through the presence of tainted variables, which are variables whose value is under the control of some untrusted client. The MARCO algorithm was published in the proceedings of the ECOOP 2005 conference. The MARCO technology is the core of IBM's Security Workbench Development Environment for Java (SWORD4J), a series of Eclipse plugins available as a free download from IBM alphaWorks.

3. ACTARUS is a static taint analysis tool that detects information-flow violations in JavaScript programs.