Verifiable Information Flow Security for AJAX Application

Description

Attacks on web browsers and other browser-like HTML rendering technologies are a significant and
increasing threat. These threats call for new software engineering strategies and new programming
language technologies. Our investigation determines how new secure language technologies can
address these new threats. By implementing a Javascript interpreter using the security-typed language,
Jif, and testing our interpreter in a live web browser, we limit the threat caused by locally executing
foreign scripts. We provide tools, models and software engineering processes for implementing secure
execution environments that handle scripts in browser-like applications. Our approach has the advantage
of automated assistance for evaluating security and produces verifiable security properties.