Caches pose a significant challenge to formal proofs of security for code executing on application processors, as the cache access pattern security-critical services may leak secret information. This paper reveals novel attack vector, exposing low-noise storage channel that can be exploited by adapting well-known timing analysis techniques. The vector also used various types software such hypervisors and monitors. uses virtual aliases with mismatched memory attributes self-modifying...

Often, an integrated mixed-criticality system is built in environment which provides separation functionality for available on-board resources. In this paper we treat such environment: the PikeOS kernel -- a commercial real-time embedded operating system. allows applications with different safety and security levels to run on same hardware. Obviously, relies correct implementation of mechanisms. context Verisoft XT TECOM projects apply deductive formal software verification mechanisms order...

5G applications with ultra-high reliability and low latency requirements necessitate the adoption of edge computing solutions in mobile networks. Container orchestration frameworks like Kubernetes (K8s) have further emerged as preferred standard to dynamically deploy on demand end-users third-party companies. Unfortunately, complex networking security concerns been highlighted challenges that impede successful container technology by industry. The challenge is exacerbated (mis-)conceptions...

Software verification tools have become a lot more powerful in recent years. Even of large, complex systems is feasible, as demonstrated the L4.verified and Verisoft XT projects. Still, functional large software rare - for reasons beyond scale effort needed due to size alone. In this paper we report on lessons learned based experience gained microkernel project. We discuss number issues that impede widespread introduction formal life-cycle process.

The isolation of security critical components from an untrusted OS allows to both protect applications and harden the itself. Virtualization memory subsystem is a key component provide such isolation. We present design, implementation verification virtualization platform for ARMv7-A processors. design based on direct paging, MMU mechanism previously introduced by Xen. It shown that this can be implemented using compact suitable formal down low level abstraction, without penalizing system...

This paper presents the first results from ongoing research project HASPOC, developing a high assurance virtualization platform for ARMv8 CPU architecture. Formal verification at machine code level guarantees information isolation between different guest systems (e.g. OSs) running on platform. To use in networking scenarios, we allow to securely communicate with each other via platform-provided communication channels and take exclusive control of peripherals outside world. The is shown be...

This paper presents an approach to provide strong assurance of the secure execution distributed event-driven applications on shared infrastructures, while relying a small Trusted Computing Base. We build upon and extend security primitives provided by Execution Environments (TEEs) guarantee authenticity integrity properties applications, control input output devices. More specifically, we that if is produced application, it was allowed be application's source code based authentic trace...

A system-of-systems (SoS) is inherently open in configuration and evolutionary lifecycle. For the next generation of cooperative cyber-physical system-of-systems, safety security constitute two key issues public concern that affect deployment acceptance. In engineering, openness nature also entail radical paradigm shifts. This paper presents one novel approach to development qualified with Cooperative Intelligent Transport Systems (C-ITS) as target. The approach, referred...

The security of embedded systems can be dramatically improved through the use formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system-level behavior, verifications need precise models underlying hardware. Such are hard to attain, highly complex, and proofs their properties may not easily apply similar but different platforms. This render verification economically infeasible. To address these issues, we...

The security of embedded systems can be dramatically improved through the use formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system level behaviour, verifications need precise models underlying hardware. Such are hard to attain, highly complex, and proofs their properties may not easily apply similar but different platforms. This render verification economically infeasible. To address these issues, we...

The concepts of information flow security and refinement are known to have had a troubled relationship ever since the seminal work McLean. In this we study refinements that support changes in data representation semantics, including addition state variables may induce new observational power or side channels. We propose epistemic approach ignorance-preserving where an abstract model is used as specification system's permitted flows, include declassification secret information. core idea...