Midlet Navigation Graphs in JML - Formal Methods: Foundations and Applications - page 17

Midlet Navigation Graphs in JML

Wojciech Mostowski and Erik Poll

Radboud University Nijmegen
Digital Security Group
[e-mail] , [e-mail]

Abstract. In the context of the EU project Mobius on Proof Carry-
ing Code for Java programs (midlets) on mobile devices, we present a
way to express midlet navigation graphs in JML. Such navigation graphs
express certain security policies for a midlet. The resulting JML specifica-
tions can be automatically checked with the static checker ESC/Java2.
Our work was guided by a realistically sized case study developed as
demonstrator in the project. We discuss practical diculties with creat-
ing ecient and meaningful JML specifications for automatic verification
with a lightweight verification tool such as ESC/Java2, and the potential
use of these specifications for PCC.

1 Introduction

Midlet navigation graph provide a way to specify security properties for Java
MIDP (Mobile Information Device Profile) applications, so-called midlets .Based
on a simpler notion of a flow graph, prescribed by the Unified Testing Criteria
(UTC) [20] to test midlets in Java Verified scheme 1 ,Cregut proposed the notion
of navigation graphs [5] as a high-level specification formalism to describe the
behaviour of Java mobile phone applications (in most cases MIDP devices are
in fact mobile phones).
Essentially, a navigation graph is a graph, or finite automaton, which describes
the ways in which an application may navigate through various screens of the
user interface, in interaction with the user and the network. Each node in the
graph represents a different screen that is displayed, e.g. a warning message
for which the user has to press 'OK' or 'Cancel', or a menu with options for
the user to choose from. The arrows between nodes represent transitions the
application can make, often in response to some user action. The graph can be
augmented with information about sensitive midlet actions, e.g. sending an SMS
or engaging in other GSM network activity. The navigation graph then gives a
high-level specification of which potentially dangerous things a given midlet does,
and under which circumstances.
In [5] Cregut gives a formal description of navigation graphs and their seman-
tics in terms of an operational semantics of Java bytecode, more specifically the
Bicolano semantics [18]. He also presents an algorithm to extract a navigation

1 http://www.javaverified.com