Abstracted for Invited and Accepted Presentations at Bytecode 2012

James Hunt - Bytecode and Safety-Critical Systems: Friend or Foe?

New standards in avionics, codify the certification of systems using object-oriented technology, interpretation, garbage collection, and formal methods, provide an opportunity for using bytecode-based languages for safety-critical development. The question remains, to what extent can bytecode be used to support rather than inhibit the use of these langauges for safety-critical development. Though experience seems to indicate that using bytecode-based languages can ease the development of complex systems, the dynamic nature of these languages complicates some conventional analysis. Certainly, efforts such as BML can facilitate the application of formal analysis techniques, but more could be done. This talk will discuss some of the problems involved and present some ideas for furthering the utility of bytecode for safety-critical systems.

Diego Garbervetsky - Quantitative analysis of Java/.Net like programs to understand heap memory requirements

There is an increasing interest in understanding and analyzing the use of resources in software and hardware systems. Certifying memory consumption is vital to ensure safety in embedded systems as well as proper administration of their power consumption; understanding the number of messages sent through a network is useful to detect performance bottlenecks or reduce communication costs, etc. Assessing resource usage is indeed a cornerstone in a wide variety of software-intensive system ranging from embedded to Cloud computing. It is well known that inferring, and even checking, quantitative bounds is difficult (actually undecidable). Memory consumption is a particularly challenging case of resource-usage analysis due to its non-accumulative nature. Inferring memory consumption requires not only computing bounds for allocations but also taking into account the memory recovered by a GC. In this talk I will present some of the work our group have been performing in order to automatically analyze heap memory requirements. In particular, I will show some basic ideas which are core to our techniques and how they were applied to different problems, ranging from inferring sizes of memory regions in real-time Java to analyzing heap memory requirements in Java/.Net. Then, I will introduce our new compositional approach which is used to analyze (infer/verify) Java and .Net programs. Finally, I will explain some limitations of our approach and discuss some key challenges and directions for future research.

Jeff Foster - Using bytecode transformation to retrofit fine-grained security policies on unmodified Android

Google's Android platform includes a permission model that protects access to sensitive capabilities, such as Internet access, GPS use, and telephony. We have found that Android's current permissions are often overly broad, providing apps with more access than they truly require. This deviation from least privilege increases the threat from vulnerabilities and malware. To address this issue, we present a novel system that can replace existing platform permissions with finer-grained ones. A key property of our approach is that it runs today, on stock Android devices, requiring no platform modifications. Moreover, we can retrofit our approach onto existing apps by transforming app bytecode to access sensitive resources through a restricted interface. We evaluated our approach on several popular, free Android apps. We found that we can replace many commonly used "dangerous" permissions with finer-grained permissions. Moreover, apps transformed to use these finer-grained permissions run largely as expected, with reasonable performance overhead.

Gabriele Costa, Giulio Caravagna, Giovanni Pardini and Luca Wiegand - Log-based Lazy Monitoring of OSGi Bundles

Lazy controllers are execution monitors which do not continuously observe the behaviour of their target. Monitors are activated and deactivated according to a scheduling strategy. When a lazy controller is activated, it checks the current security state and, in case of a violation, terminates the execution. Instead, if the current execution trace is safe, the monitor is suspended and its activation is scheduled again. The inactivity period is computer by considering the risk that, from the current state, the target can produce a security violation. This behaviour is particularly interesting for systems which are difficult to monitor with standard approaches, such as web services. In this paper we present a prototype using existing logging API, i.e., the Commons Logging Package, for remotely watching the execution of OSGi bundles. We claim that our solution can efficiently follow the target system keeping under control the delay in detecting violations. Also, as we use standard OSGi platform and facilities, we show that our monitors can run under very realistic assumptions in the context of web services.

Elvira Albert, Samir Genaim and Guillermo Román-Díez - Conditional Termination of Loops over Arrays

This paper studies conditional termination of loops that involve array accesses, including loops which traverse circularly arrays, loops which use as loop bound or as loop counter an array element, etc. This kind of loops are commonly used, and their termination can only be proven if array contents are tracked. We present a new termination analysis for sequential bytecode programs which performs three main steps: (1) it first statically infers whether the memory locations of arrays remain constant along the execution of the loop and also whether there are aliases to such locations; (2) based on the inferred information, we provide sufficient conditions which guarantee if array accesses can be transformed into local variables; (3) when the conditions cannot be proven, we generate conditional termination assertions which, if satisfied, termination is guaranteed.

Michael Barnett and Shaz Qadeer - BCT: A translator from MSIL to Boogie

We describe the design and implementation of BCT, a translator from Microsoft MSIL into Boogie, a verification language that in turn targets SMT (Satisifiability-Modulo-Theories) solvers. BCT provides a vechicle for converting any program checker for the Boogie programming language into a checker for a language that compiles to Microsoft's .NET platform. BCT is methodology-neutral, precise in encoding the operational semantics of the .NET runtime, and comprehensively covers all features of .NET.

Olga Gadyatskaya, Eduardo Lostal and Fabio Massacci - Extended Abstract: Embeddable Security-by-Contract Verifier for Java Card

Modern multi-application smart cards based on the Java Card technology can become an integrated environment where applications from different providers are loaded on the fly and collaborate in order to facilitate lives of the cardholders. This initiative requires an embedded verification mechanism to ensure that all applications on the card respect the application interactions policy. The Security-by-Contract (SxC) approach for loading time verification consists of two phases. During the first phase the loaded bytecode is verified to be compliant with the supplied contract. Then, during the second phase the contract is matched with the smart card security policy. In the paper we report about implementation of a SxC prototype, present the memory statistics that justifies the potential of this prototype to be embedded on an actual device and discuss the SxC prototype for testing purposes that can be run on a PC.

Henrik Søndberg Karlsen, Erik Ramsgaard Wognsen, Mads Chr. Olesen and René Rydhof Hansen - Study, Formalisation, and Analysis of Dalvik Bytecode

With the large, and rapidly increasing, number of smartphones based on the Android platform, combined with the open nature of the platform that allows ``apps'' to be downloaded and executed on the smartphone, misbehaving and malicious (malware) apps is set to become a serious problem. To counter this problem, automated tools for analysing and verifying apps are essential. Further, to ensure high-fidelity of such tools, we believe that it is essential to formally specify both semantics and analyses. In this paper we present the first (to the best of our knowledge) formalisation of the Dalvik bytecode language and formally specified control flow analysis for the language. To determine which features to include in the formalisation and analysis, 1,700 Android apps from the Android Market were downloaded and examined.
Last modified: Tue Jan 31 15:11:32 CET 2012