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

To ultimately use our approach in a PCC scenario, it has to be possible to
distinguish the JML annotations expressing the desired security policy (i.e. the
navigation graph) from any additional JML annotations that are needed for the
verification to go through. For the former we must check that these really express
the security policy we want. For the latter we do not: we don't care what these
are, as long as the proof goes through.
It seems possible to make this distinction here. However, the JML annotations
expressing the desired security policy - thenavigationgraph-dohavetorefer
to program variables (namely the Displayable s that the program uses), so we
cannot quite have these annotations - our “policy” - completely independent of
the midlet code.
Also, a malicious midlet could contain specification statements ( set -state-
ments) that affect the values of the ghost state used in the API specification,
making any certification meaningless; it would have to be checked that there are
no such statements in the midlet code.
Of course, to then verify and provide PCC certificates for midlets, instead of
using ESC/Java2, one should use a sound verification approach that can provide
proofs (certificates) [2].
Acknowledgements. This work is supported by the MOBIUS project in the
Information Society Technologies programme of the European Commission and
the CHARTER project in the ARTEMIS Embedded Computing Systems Initia-
tive. We would also like to thank the anonymous reviewers for their insights.
References
1. Barnett, M., Leino, K., Schulte, W.: The Spec# programming system: An overview.
In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS
2004. LNCS, vol. 3362, pp. 151-171. Springer, Heidelberg (2005)
2. Barthe, G., Cregut, P., Gregoire, B., Jensen, T., Pichardie, D.: The MOBIUS proof
carrying code infrastructure. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de
Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 1-24. Springer, Heidelberg
(2008)
3. Beckert, B., Hahnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Soft-
ware: The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
4. Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced spec-
ification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue,
M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342-363.
Springer, Heidelberg (2006)
5. Cregut, P.: Extracting control from data: User interfaces of MIDP applications.
In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol. 4912,
pp. 41-56. Springer, Heidelberg (2008)
6. Drossopoulou, S., Francalanza, A., Muller, P., Summers, A.: A unified framework
for verification techniques for object invariants. In: Ryan, M. (ed.) ECOOP 2008.
LNCS, vol. 5142, pp. 412-437. Springer, Heidelberg (2008)
7. Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended
static checking for Java. In: PLDI 2002, pp. 234-245. ACM, New York (2002)