TY - GEN
T1 - Functional "AJAX" in secure synchronous programming
AU - Mukhopadhyay, Supratik
AU - Bharadwaj, Ramesh
AU - Davulcu, Hasan
PY - 2011/3/28
Y1 - 2011/3/28
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=79952947531&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=79952947531&partnerID=8YFLogxK
U2 - 10.1109/HICSS.2011.210
DO - 10.1109/HICSS.2011.210
M3 - Conference contribution
AN - SCOPUS:79952947531
SN - 9780769542829
T3 - Proceedings of the Annual Hawaii International Conference on System Sciences
BT - Proceedings of the 44th Annual Hawaii International Conference on System Sciences, HICSS-44 2010
T2 - 44th Hawaii International Conference on System Sciences, HICSS-44 2010
Y2 - 4 January 2011 through 7 January 2011
ER -