On the Systematic Design of Web Languages
Abstract
The emergence of "web languages," such as Java, support the development of programs that can be downloaded to a client's machine for execution by a web browser. This brings power and flexibility to web applications, but it also brings well-known end-point security problems, such as the threat of integrity and unauthorized disclosure attacks. Yet although security has been an issue in web language design, there appears to be no formal characterization of the kinds of security properties that one can expect of programs written in these languages. A web language should be designed so that all programs are guaranteed to satisfy explicitly stated security properties. To this end, the authors advocate a more systematic approach to the design of secure web languages. One begins with a core language for which some set of desired security properties can be shown to hold with respect to a formal semantics. The language is then incrementally extended to include new features, as necessary. At each step, the designer has an obligation to establish that the security properties have been preserved. For example, one kind of attack a web language should guard against is a disclosure attack, where a malicious program downloaded by a client attempts to make the contents of certain private files public. There is a form of static analysis that can be applied to programs to protect against disclosure attacks while allowing utilities like mail tools to access files and directories at different sensitivity levels. It is called "secure information flow" analysis. The authors briefly describe how a type system can be imposed on a simple imperative language to guarantee secure information flow. In part, they illustrate how well type theory can be applied to address a security problem, but their main point is that the security theorem stated here actually guides the language designer in evaluating potential language extensions.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1996
- Accession Number
- ADA484193
Entities
People
- Dennis Volpano
- Geoffrey B. Smith
Organizations
- Naval Postgraduate School