Information Technology Reference
In-Depth Information
1527 lines of code in the main file of the original Java semantics. The abstract
operational Java semantics was developed as a source-to-source transformation
in rewriting logic and consists of 650 lines of extra code. This is equivalent to
saying that, in our current system, the
trusted computing base
(TCB)
5
is less
than a fourth of the size of the original Java semantics (at least one order of
magnitude smaller than the standard rewriting infrastructure, and even much
smaller than other PCC systems).
Since our approach is based on a rewriting logic semantics specification of
the full Java 1
.
4 language [18], the methodology developed in this work can be
easily extended to cope with exceptions, heaps, and multithreading since they
are considered in the Java rewriting logic semantics.
References
1. Alba-Castro, M., Alpuente, M., Escobar, S.: Automatic certification of Java source
code in rewriting logic. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916,
pp. 200-217. Springer, Heidelberg (2008)
2. Alba-Castro, M., Alpuente, M., Escobar, S.: Automated certification of non-
interference in rewriting logic. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008.
LNCS, vol. 5596, pp. 182-198. Springer, Heidelberg (2009)
3. Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-
oriented programs. In: Conference record of the 33rd ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2006, pp. 91-102
(2006)
4. Barbuti, R., Bernardeschi, C., Francesco, N.D.: Abstract interpretation of opera-
tional semantics for secure information flow. Information Processing Letters 83(22),
101-108 (2002)
5. Barthe, G., D'Argenio, P., Rezk, T.: Secure information flow by self-composition.
In: Proceedings of the 17th IEEE workshop on Computer Security Foundations,
CSFW 2004, pp. 100-114 (2004)
6. Bavera, F., Bonelli, E.: Type-based information flow analysis for bytecode lan-
guages with variable object field policies. In: SAC 2008, pp. 347-351 (2008)
7. Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Proc. IEEE Computer Se-
curity Foundations Symposium, CSF 2008 (2008)
8. Clavel, M., Duran, F., Eker, S., Lincoln, P., Mart ı-Oliet, N., Meseguer, J., Talcott,
C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS,
vol. 4350. Springer, Heidelberg (2007)
9. Cousot, P., Cousot, R.: Systematic Design of Program Analysis Frameworks. In:
Proc. of Sixth ACM Symp. on Principles of Programming Languages, pp. 269-282
(1979)
10. Darvas, A., Hahnle, R., Sands, D.: A theorem proving approach to analysis of secure
information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450,
pp. 193-209. Springer, Heidelberg (2005)
11. Denning, D.E., Denning, P.J.: Certification of programs for secure information flow.
Commun. ACM 20(7), 504-513 (1977)
5
The TCB is the part of the code that is used to check if other code can be safely
run, and it is assumed to be trusted.
