Logo: to the web site of Uppsala University

Contracts capture assumptions (preconditions) and guarantees (postconditions) of functions in a software program, and are an important paradigm for documenting program code, for program understanding, and to enable modular program verification. In this paper, we focus on contracts for stateful software modules, for instance modules implementing data-structures like queues. Such modules offer different kinds of functions to their environment: observers, which are pure functions used to query the state of the module; and mutators, which can change the module state. We present a novel technique to synthesize contracts for the mutators of a module, in which pre- and postconditions are expressed as Boolean combinations of the observers. Our method builds on existing algorithms for active learning of register automata to model the possible behaviours of the stateful module. We then present techniques for synthesizing contracts from a learned register automaton. The entire method is fully black-box and automated. Based on our proposed approach, we develop a tool called CoGent that generates a set of contracts for a mutator from a given register automaton of a module. Finally, we evaluate our tool using the APIs for various data structures.

Web browser-based applications deal with humongous user information using applications of web scripts. In particular, JavaScript applications access information through built-in browser APIs that dynamically load remote scripts and execute with the same privilege as that of the applications - usually referred to as mashup model. Unfortunately, this allows malicious JavaScripts to manipulate the given browser functionalities leading to various web attacks violating users' privacy. Moreover, with the rapid growth of e-commerce sectors, malicious scripts pose a significant challenge to digital transactions. In this paper, we propose an approach that prevents various web-based attacks such as code injection, cross-site scripting (XSS). The approach adopts a Dynamic Labelling algorithm that generates information flow security policies automatically for local variables in JavaScript based on the given policies for sensitive variables. Unlike existing solutions that are too conservative primarily due to the generic flow policies leading to false-alarms, our solution leads to realizing conditions as to when a script accepts the parameters returned by a dynamic script; thus enabling us to build an automatic platform for preventing information flows to malicious scripts without explicit characterization by programmers or users.