Abstract:
Research on security techniques for Java bytecode
has paid little attention to the security of the implementations
of the techniques themselves, assuming
that ordinary tools for programming, verification
and testing are sufficient for security.
However, different categories of security policies
and mechanisms usually require different implementations.
Each implementation requires extensive
effort to test it and/or verify it.
We show that programming with well-typed
pattern structures in a statically well-typed language
makes it possible to implement static bytecode
verification in a fully type-safe and highly
adaptive way, with security policies being fed in
as first-order parameters, reduces the effort required
to verify security of an implementation itself
and the programming need for new policies.
Also bytecode instrumentation can be handled in
exactly the same way. The approach aims at reducing
the workload of building and understanding
distributed systems, especially those of mobile
code.
