SHOW publication #299 - ABLE Publications

Analysis at the level of a runtime architecture matches the way experts reason about security or privacy better than a purely code-based strategy. However, the architecture must still be correctly realized in the implementation. We previously developed Scholia to analyze, at compile time, communication integrity between arbitrary object-oriented code, and a rich, hierarchical intended runtime architecture, using typecheckable annotations. This paper applies Scholia to security runtime architectures. Having established traceability between the target architecture and the code, we extend Scholia to enforce structural architectural constraints. At the code level, annotations enforce local, modular constraints. At the architectural level, predicates enforce global constraints. We validate the end-to-end approach in practice using a real 3,000-line Java implementation, and enforce its conformance to a security architecture designed by an expert.