Instrumenting legacy code is an effective approach to enforce security policies. Formal correctness of this approach in the realm of audit logging relies on semantic frameworks that leverage information algebra to model and compare the information content of the generated audit logs and the program at runtime. Previous work has demonstrated the applicability of instrumentation techniques in the enforcement of audit logging policies for systems with microservices architecture. However, the specified policies suffer from the limited expressivity power as they are confined to Horn clauses being directly used in logic programming engines. In this paper, we explore audit logging specifications that go beyond Horn clauses in certain aspects, and the ways in which these specifications are automatically enforced in microservices. In particular, we explore an instrumentation tool that rewrites Java-based microservices according to a JSON specification of audit logging requirements, where these logging requirements are not limited to Horn clauses. The rewritten set of microservices are then automatically enabled to generate audit logs that are shown to be formally correct.

Information-algebraic models have been shown as effective semantic frameworks in the specification of audit logging requirements. These semantic frameworks underlie implementation models that formally guarantee correctness of audit logs. Recently, one such implementation model has been proposed for concurrent systems. In this paper, we study the deployment of an instrumentation tool based on this implementation model, aiming at microservices-based applications that are built by Java Spring framework. This tool instruments these applications according to a given logging specification, described in JSON. A set of events in one or more microservices may necessitate the generation of log entries in a specific microservice. Instrumentation of an application enables different microservices of that application to concurrently generate audit logs.

This paper presents a novel implementation of an augmented reality-aided indoor navigation system for mobile devices. The proposed system uses the device's camera to scan the environment, generate an abstracted 3D map of the indoor environment, and transfer it to a remote server. The 3D map of the indoor environment is achieved through a tracking and mapping ARKit module. Once the indoor map is stored in the server, it can be accessed simultaneously by multiple devices for localization and navigation. Leveraging Unity assets and the directions retrieved from the server, the application computes the shortest distance between the source and destination, and displays AR-based direction markers for navigation assistance.

Dynamic taint analysis is often used as a defense against low-integrity data in applications with untrusted user interfaces. An important example is defense against XSS and injection attacks in programs with web interfaces. Data sanitization is commonly used in this context, and can be treated as a precondition for endorsement in a dynamic integrity taint analysis. However, sanitization is often incomplete in practice. We develop a model of dynamic integrity taint analysis for Java that addresses imperfect sanitization with an in-depth approach. To avoid false positives, results of sanitization are endorsed for access control (aka prospective security), but are tracked and logged for auditing and accountability (aka retrospective security). We show how this heterogeneous prospective/retrospective mechanism can be specified as a uniform policy, separate from code. We then use this policy to establish correctness conditions for a program rewriting algorithm that instruments code for the analysis. These conditions synergize our previous work on the semantics of audit logging with explicit integrity which is an analogue of noninterference for taint analysis. A technical contribution of our work is the extension of explicit integrity to a high-level functional language setting with structured data, vs. previous systems that only address low level languages with unstructured data. Our approach considers endorsement which is crucial to address sanitization. An implementation of our rewriting algorithm is presented that hardens the OpenMRS medical records software system with in-depth taint analysis, along with an empirical evaluation of the overhead imposed by instrumentation. Our results show that this instrumentation is practical.