Abstract: The Mobius verification environment supports the development of specifications, programs and proofs of their security properties. It supports both source code and bytecode-level verification, and will be able to produce the output necessary for the generation of PCC certificates.

The Mobius PVE is a customized version of the Eclipse platform that integrates a set of tools that support software development using state-of-the-art formal methods and software engineering techniques. The Mobius PVE supports the specification and verification of JML-annotated Java programs at the source code level as well as at the bytecode level using logic- and type-based techniques and the Proof-Carrying Code paradigm. The properties of particular interest include security (e.g. data is secret and never leaked) and resource guarantee properties (e.g. this method will never use more than this much memory or that much CPU) as well as total functional correctness. The Mobius PVE is thus, in a sense, a prototype realization of the U.K. Grand Challenge 6 Verifying Compiler, specialized to the domain of Java programs (HM05).

The Mobius PVE integrates theoretical and technical best-practices, leveraging the hard work of many research groups within, as well as outside of, the MOBIUS grant consortium. Many Java software engineers use the Eclipse development environment, together with plugins such as FindBugs and PMD. The Mobius PVE is bundled with Eclipse and these well-known third-party plugins so that Java developers are presented with a pre-configured development environment without the need to manually install each plugin.

This talk summarizes the current and planned capabilities of the Mobius PVE and the Mobius Verification Bus. It is written for potential and current Mobius PVE users, verification researchers, and verification tool developers.