Mobius: Mobility, Ubiquity and Security
Proof-carrying code for Java on mobile devices
Mobius is a European Integrated Project developing novel technologies for
trustworthy global computing, using proof-carrying code
to give users
independent guarantees of the safety and security of
applications for their mobile phones and PDAs.
Global computing means that applications today may run anywhere, with data and
code moving freely between servers, PCs and other devices: this kind of
mobility over the ubiquitous internet magnifies the challenge of making sure
that such software runs safely and reliably. In this context, the Mobius
project focuses on securing applications downloaded to the
Java MIDP platform
deployed across a host of phones, this is the common runtime environment for a
myriad mobile applications.
Techniques of static analysis
make it possible to check program behaviour by
analysing source code before it ever executes. But mobile code mean that this
assurance must somehow travel with the application to reach the user.
Conventional digital signatures use cryptography to identify who supplied a
program; the breakthrough of proof-carrying code
to give mathematical proofs that guarantee the security of the code itself.
We can strengthen digital signatures with digital evidence.
Key features of the Mobius security architecture are:
- Innovative trust management, with digital evidence of program behaviour
that can be independently checked by users or any third party.
- Static enforcement, checking code before it starts; adaptable to manage a
range of user security concerns, and configurable to match the real-world
mix of mobile platforms.
- Modularity, allowing developers to build up trusted applications from
The PCC paradigm is known for decentralized trust management, but has generally been restricted to simple safety properties, and to monolithic, non-distributed applications. We shall pioneer the first PCC framework applicable to global computers, and the first to allow enforcement of functional properties as well as advanced security properties. We shall extend the two technologies that enable PCC - type systems and program logics - to allow enforcement of more advanced security properties, and combine them in hybrid certificates to be checked through type checking together with
|| Modern verification environments based on program logics typically operate on source programs. The Mobius project proposes to combine these environments with type systems, which provide an automated means to enforce many basic policies, and use the resulting framework to cover a wide range of security policies for global computers. Evidence of programs adherence to their policy will be recorded by certificates: condensed, easily checkable formal proofs. In order to bring the benefits of source code verification to the code consumers, compilers will be enhanced to transform specifications and proofs for bytecode programs, yielding certificates that establish the correctness of bytecode programs and can be checked efficiently by code consumers.