Functional "AJAX" in Secure Synchronous Programming

AJAX (Asynchronous Javascript and XML) is a confederation of technologies aimed at providing improved user interaction with web-based applications. While AJAX provides an improved user experience, it also comes with its baggage of problems. The lack of formal semantics makes AJAX applications difficult to build, debug, understand, and validate. Different component technologies of AJAX (e.g., XMLHttpRequest or Javascript) are browser-sensitive and have different implementations and provide distinct functionalities. Source code is downloaded and run on the clients machines, raising security concerns. In this paper, we present an ``AJAX´´-like framework in an event-driven secure synchronous programming environment. Our framework is supported by a formal operational semantics. Applications written in our language can be verified using formal static analysis techniques such as theorem proving. The applications are compiled and run on the SINS (Secure Infrastructure for Networked Systems) infrastructure jointly developed in collaboration with the Naval Research Laboratory.