P. Ferrara.
JAIL: Firewall Analysis of Java Card by Abstract Interpretation

In Proceedings of the 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI 2006), Vienna, Austria, March 26, 2006

Final version: Pdf (244 KB)
Slides: Pdf (439 KB)

Abstract: We introduce JAIL, a tool for the static analysis and the verification of the applet isolation property of Java Card, where applet isolation means that one applet cannot access the fields or objects of an applet in another context unless the other applet explicitly provides an interface for access. The tool statically checks whether the analyzed source code violates this property, thus detecting if SecurityExceptions are possibly raised in the JCRE.

Bibtex:

@inproceedings{Ferr06,
  author = {Pietro Ferrara},
  title = {JAIL: Firewall Analysis of Java Card by Abstract Interpretation},
  booktitle = {Proceedings of the 1st International Workshop on Emerging
               Applications of Abstract Interpretation ({EAAI 2006})},
  month = mar,
  year = {2006},
}