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.
M.Huisman@utwente.nl
Last modified: Tue Jan 31 15:11:32 CET 2012