Cloud programming is one of the major factors that shape how large-scale distributed applications will be structured and executed on the future Internet. This paradigm shift in the development of Internet-based applications is readily apparent by the server-side changes that it entails; unsurprisingly, there is numerous corresponding research work. The changes to the client-side programming and usage of such applications, however, is also fundamental and profound but have been the subject of much less attention.
2. Static and dynamic analysis of web scripting programming languages;
3. Preventive Information Flow Control through a Mechanism of Split Addresses.
This work is composed into two parts: JSCert, which has been written in an eye-verifiable correspondence to be closed to the EcmaScript 5 specification; and JSRef, a Coq interpreter which has been proved correct with respect to JSCert.
We now aim to build certified tools from JSCert. As JSCert itself is already huge, we do not plan to only use it to prove our analyser, but also to build it. To this end, we are adapting abstract interpretation to pretty-big-step semantics, which is the basis of JSCert. The final goal is to automatically get a correct-by-construction abstract interpreter from some manually defined lattices and abstractions.
2. Static and dynamic analysis of web scripting programming languages
In connection with integrating static and dynamic analysis, a crucial question concerns the flow of information between the applications and the system. System-level monitoring is currently the only existing technique for detecting a violation of the security policy based on several file read and write operations and the experience of the CIDre team has shown the viability of monitoring of applications at system level in classical operating systems. The main challenge will be to combine static analysis and dynamic analysis at the application and system level in the setting of novel, web-oriented execution platforms, taking into account the results obtained in the third activity on multi-level information flow monitoring. These results notably concern how static and dynamic security verification can be architectured from applications via the browser down to the OS level.
3. Preventive Information Flow Control through a Mechanism of Split Addresses
The current state of the Internet and web technologies makes it extremely appealing to the vast majority of the computerized world to depend on purely on-line services. The advent of HTML5 has triggered an array of approaches increasing the feature set of web applications. Some of these novel technologies such as CORS, cross-document messaging, WebRTC or web sockets, allow for communication on web pages on levels that were not feasible earlier. Others such as IndexedDB and local storage increase client side storage capabilities. This has led to an increasing need to improve the security of the web-browsers. These techniques stress on the need to monitor these new possibilities of information leakages since the web pages are converging to the functionalities traditionally reserved for desktop applications.
Over the years, there have been a lot of improvements including the key conceptualization of same-origin policy. Despite all these current safeguards, constant threats to web-services prevail, thereby, increasing the desire for security enhancements to help in the progression towards a better Internet. Some of the most prominent vulnerabilities such as cross-site scripting (XSS) and cross-site request forgery (CSRF) feature in the OWASP Top Ten. These attacks can be characterized by malicious information flows and hence information flow control (IFC) is an effective methodology to counter them.
Our model for preventive enforcement is called the "Address Split Design". The idea is to have two address spaces for each sensitive variable. The private address space contains the secret values and the public address space contains a dummy value. The private address is provided to the functions with the necessary privileges. A small illustration of our model is provided below.
We perceive that the loss of functionality must be minimized despite the need for stronger security mechanisms. Our model is in line with this philosophy and the results of our analysis will follow.
Keep following us on this page and kindly check our publications & results for more information.