An Abstract Semantics for Inference of Types and Effects in a Multi-Tier Web Language

TL;DR

This paper uses abstract interpretation to analyze and correct a types-and-effects system for a multi-tier web language, ensuring soundness in security-related static analysis.

Contribution

It reconstructs a types-and-effects system using abstract interpretation, identifies soundness issues, and provides a corrected, systematic analysis approach.

Findings

Original system was not sound with language semantics

Corrected analysis achieves soundness

Framework can be applied to security analysis in web languages

Abstract

Types-and-effects are type systems, which allow one to express general semantic properties and to statically reason about program's execution. They have been widely exploited to specify static analyses, for example to track computational side effects, exceptions and communications in concurrent programs. In this paper we adopt abstract interpretation techniques to reconstruct (following the Cousot's methodology) a types-and-effects system developed to handle security problems of a multi-tier web language. Our reconstruction allows us to show that this types-and-effects system is not sound with respect to the semantics of the language. In addition, we correct the soundness issues in the analysis and systematically construct a correct analyser.