scholarly journals Compositional Verification of Security Properties for Embedded Execution Platforms

10.29007/h4rv ◽  
2018 ◽  
Author(s):  
Christoph Baumann ◽  
Oliver Schwarz ◽  
Mads Dam
Keyword(s):  
Embedded System ◽  
Message Passing ◽  
Theorem Prover ◽  
System Level ◽  
Compositional Verification ◽  
System Specification ◽  
Security Proof ◽  
Security Properties ◽  
On Chip ◽  
High Level

The security of embedded systems can be dramatically improved through the use of formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system level behaviour, the verifications need precise models of the underlying hardware. Such models are hard to attain, highly complex, and proofs of their security properties may not easily apply to similar but different platforms. This may render verification economically infeasible.To address these issues, we propose a compositional top-down approach to embedded system specification and verification, where the system-on-chip is modeled as a network of distributed automata communicating via paired synchronous message passing. Using abstract specifications for each component allows to delay the development of detailed models for cores, devices, etc., while still being able to verify high level security properties like integrity and confidentiality, and soundly refine the result for different instantiations of the abstract components at a later stage.As a case study, we apply this methodology to the verification of information flow security for an industry scale security-oriented hypervisor on the ARMv8-A platform. The hypervisor statically assigns (multiple) cores to each guest system and implements a rudimentary, but usable, inter guest communication discipline. We have completed a pen-and-paper security proof for the hypervisor down to state transition level and report on a partially completed verification of guest mode security in the HOL4 theorem prover.

Model-Driven Design and ASM-Based Validation of Embedded Systems

2010 ◽  
pp. 24-54 ◽  
Author(s):  
Angelo Gargantini ◽  
Elvinia Riccobene ◽  
Patrizia Scandurra
Keyword(s):  
Embedded System ◽  
Graphical Models ◽  
Code Generation ◽  
Formal Method ◽  
System Level ◽  
Levels Of Abstraction ◽  
Model Driven ◽  
The Embedded System ◽  
On Chip ◽  
High Level

In the embedded system and System-on-Chip (SoC) design area, the increasing technological complexity coupled with requests for more performance and shorter time to market have caused a high interest for new methods, languages and tools capable of operating at higher levels of abstraction than the conventional system level. This chapter presents a model-driven and tool-assisted development process of SoCs, which is based on high-level UML design of system components, guarantees SystemC code generation from graphical models, and allows validation of system behaviors on formal models automatically derived from UML models. An environment for system design and analysis is also presented, which is based on a UML profile for SystemC and the Abstract State Machine formal method.

scholarly journals A Signature-Based Power Model for MPSoC on FPGA

VLSI Design ◽  
2012 ◽  
Vol 2012 ◽  
pp. 1-13 ◽  
Author(s):  
Roberta Piscitelli ◽  
Andy D. Pimentel
Keyword(s):  
Design Space Exploration ◽  
Design Space ◽  
Power Estimation ◽  
System Level ◽  
Estimation Methods ◽  
Instruction Set ◽  
Systems On Chip ◽  
Event Signatures ◽  
On Chip ◽  
High Level

This paper presents a framework for high-level power estimation of multiprocessor systems-on-chip (MPSoC) architectures on FPGA. The technique is based on abstract execution profiles, called event signatures, and it operates at a higher level of abstraction than, for example, commonly used instruction-set simulator (ISS)-based power estimation methods and should thus be capable of achieving good evaluation performance. As a consequence, the technique can be very useful in the context of early system-level design space exploration. We integrated the power estimation technique in a system-level MPSoC synthesis framework. Subsequently, using this framework, we designed a range of different candidate architectures which contain different numbers of MicroBlaze processors and compared our power estimation results to those from real measurements on a Virtex-6 FPGA board.

PERFORMANCE ANALYSIS OF A JPEG ENCODER MAPPED ONTO A VIRTUAL MPSoC-NoC ARCHITECTURE USING TLM 2.0.1

2013 ◽  
Vol 22 (05) ◽  
pp. 1350036
Author(s):  
F. A. ESCOBAR-JUZGA ◽  
F. E. SEGURA-QUIJANO
Keyword(s):  
Message Passing ◽  
Programming Model ◽  
Task Graph ◽  
Modeling Tools ◽  
Networks On Chip ◽  
Hardware Description ◽  
On Chip ◽  
Network Speed ◽  
High Level ◽  
The Impact

Networks on Chip (NoCs) are commonly used to integrate complex embedded systems and multiprocessor platforms due to their scalability and versatility. Modeling tools used at the functional level use SystemC to perform hardware–software co-design and error correction concurrently, thus, reducing time to market. This work analyzes a JPEG encoding algorithm mapped onto a configurable M × N, mesh/torus, NoC platform described in SystemC with the transaction level modeling (TLM) standard; timing constraints for both, the router and network interface controller, are assigned according to a hardware description language (HDL) model written for this purpose. Processing nodes are also described as SystemC threads and their computation delays are assigned depending on the amount and cost of the operations they perform. The programming model employed is message passing. We start by describing and profiling the JPEG algorithm as a task graph; then, four partitioning proposals are mapped onto three NoCs of different size. Our analysis comprises changes in topology, virtual channel depth, routing algorithms, network speed and task-node assignments. Through several high-level simulations we evaluate the impact of each parameter and we show that, for the proposed model, most improvements come from the algorithm partitioning.

scholarly journals Accurate Model for Network-on-Chip Performance Evaluation Based on Timed Colored Petri Net

2016 ◽  
Vol 11 (2) ◽  
pp. 75-85
Author(s):  
J. Silveira ◽  
A. Cadore ◽  
G. Barroso ◽  
C. Marcon ◽  
T. Webber ◽  
...  
Keyword(s):  
Petri Net ◽  
Time Estimation ◽  
Network On Chip ◽  
System Level ◽  
Colored Petri Net ◽  
Accurate Analysis ◽  
Estimation Errors ◽  
On Chip ◽  
Buffer Length ◽  
High Level

Network-on-Chip (NoC) is a power architecture that emerged to solve communication issues present in modern Systems-on-Chip (SoCs). NoC based architectures are very scalable and offer high levels of communication parallelism, among other features. Every efficient NoC implementation requires several design steps to accomplish indices of performance. Although there are many system level models, high-level models for NoC are representative in the context of design since they provide fast and accurate analysis, with low modeling effort, for further VHDL implementations. This work proposes a NoC model based on a Timed Colored Petri Net (TCPN) that computes performance indices seamlessly. Network latency and buffer occupation are of special interest in our approach as they represent the key indices when assessing NoC performance. As results, we have validated and refined the model of a 5×5 mesh NoC comparing its indices with equivalent VHDL RTL description under synthetic and real traffic situations. The proposed model is capable of analyzing the influence of the router service time on the average latency time, enabling internal NoC evaluation to optimize buffer length. Simulation results demonstrate the model suitability for latency evaluation with time estimation errors often below 1%. Furthermore, this paper discusses the effort required to extend the model with other NoC architectural features. We conclude that the use of a TCPN model of NoC generates accurate results providing as much detailed information as their equivalent experiments using VHDL description.

scholarly journals An Approach for Power Estimation at Electronic System Level using Distributed Simulation

2016 ◽  
Vol 11 (3) ◽  
pp. 159-170
Author(s):  
Helder F. A. Oliveira ◽  
Alisson V. Brito ◽  
Joseana M. F. R. Araujo ◽  
Elmar U. K. Melcher
Keyword(s):  
Distributed Simulation ◽  
Power Estimation ◽  
Electronic System ◽  
System Level ◽  
Multiprocessor System ◽  
High Level Architecture ◽  
Electronic System Level ◽  
On Chip ◽  
High Level ◽  
Abstraction Levels

The present research aims to develop an approach using HLA (High Level Architecture), enabling the cre-ation of a distributed and heterogeneous environment, composed by different tools and models to obtain a better trade-off between accuracy and run time in power estimation. These models can be described in different languages and/or abstraction levels, as well as use different power estimation approaches. The use of HLA enables the synchronized and distributed simulation of the elements that compose the simulation environment. The approach must allow the collecting and grouping of power estimation data in a centralized manner. As a case study, an MPSoC (MultiProcessor System-on-Chip) ESL/TLM model, described in C++/SystemC, and an ESL model, created on Ptolemy framework, have been used. The experimental results show the flexibility of the approach, which promotes an integrated view of power estimation data.

scholarly journals Aircraft Requirements for Sustainable Regional Aviation

Aerospace ◽  
2021 ◽  
Vol 8 (3) ◽  
pp. 61
Author(s):  
Dominik Eisenhut ◽  
Nicolas Moebs ◽  
Evert Windels ◽  
Dominique Bergmann ◽  
Ingmar Geiß ◽  
...  
Keyword(s):  
Systems Engineering ◽  
System Level ◽  
Policy Initiative ◽  
The European Union ◽  
Calculation Methods ◽  
Figures Of Merit ◽  
Performance Requirements ◽  
High Level ◽  
Different Levels ◽  
The Eu

Recently, the new Green Deal policy initiative was presented by the European Union. The EU aims to achieve a sustainable future and be the first climate-neutral continent by 2050. It targets all of the continent’s industries, meaning aviation must contribute to these changes as well. By employing a systems engineering approach, this high-level task can be split into different levels to get from the vision to the relevant system or product itself. Part of this iterative process involves the aircraft requirements, which make the goals more achievable on the system level and allow validation of whether the designed systems fulfill these requirements. Within this work, the top-level aircraft requirements (TLARs) for a hybrid-electric regional aircraft for up to 50 passengers are presented. Apart from performance requirements, other requirements, like environmental ones, are also included. To check whether these requirements are fulfilled, different reference missions were defined which challenge various extremes within the requirements. Furthermore, figures of merit are established, providing a way of validating and comparing different aircraft designs. The modular structure of these aircraft designs ensures the possibility of evaluating different architectures and adapting these figures if necessary. Moreover, different criteria can be accounted for, or their calculation methods or weighting can be changed.

scholarly journals Integrated Magnetohydrodynamic Pump with Magnetic Composite Substrate and Laser-Induced Graphene Electrodes

Polymers ◽  
2021 ◽  
Vol 13 (7) ◽  
pp. 1113
Author(s):  
Mohammed Asadullah Khan ◽  
Jürgen Kosel
Keyword(s):  
Magnetic Flux ◽  
Flow Rate ◽  
Magnetic Composite ◽  
Propulsive Force ◽  
Closed Channel ◽  
Lab On Chip ◽  
Composite Substrate ◽  
On Chip ◽  
High Level ◽  
Moving Parts

An integrated polymer-based magnetohydrodynamic (MHD) pump that can actuate saline fluids in closed-channel devices is presented. MHD pumps are attractive for lab-on-chip applications, due to their ability to provide high propulsive force without any moving parts. Unlike other MHD devices, a high level of integration is demonstrated by incorporating both laser-induced graphene (LIG) electrodes as well as a NdFeB magnetic-flux source in the NdFeB-polydimethylsiloxane permanent magnetic composite substrate. The effects of transferring the LIG film from polyimide to the magnetic composite substrate were studied. Operation of the integrated magneto hydrodynamic pump without disruptive bubbles was achieved. In the studied case, the pump produces a flow rate of 28.1 µL/min. while consuming ~1 mW power.

CSim 2

2021 ◽  
Vol 43 (1) ◽  
pp. 1-46
Author(s):  
David Sanan ◽  
Yongwang Zhao ◽  
Shang-Wei Lin ◽  
Liu Yang
Keyword(s):  
Programming Languages ◽  
Concurrent Systems ◽  
Theorem Prover ◽  
Compositional Techniques ◽  
Machine Code ◽  
Top Down ◽  
Hol Theorem Prover ◽  
High Level ◽  
High Degree

To make feasible and scalable the verification of large and complex concurrent systems, it is necessary the use of compositional techniques even at the highest abstraction layers. When focusing on the lowest software abstraction layers, such as the implementation or the machine code, the high level of detail of those layers makes the direct verification of properties very difficult and expensive. It is therefore essential to use techniques allowing to simplify the verification on these layers. One technique to tackle this challenge is top-down verification where by means of simulation properties verified on top layers (representing abstract specifications of a system) are propagated down to the lowest layers (that are an implementation of the top layers). There is no need to say that simulation of concurrent systems implies a greater level of complexity, and having compositional techniques to check simulation between layers is also desirable when seeking for both feasibility and scalability of the refinement verification. In this article, we present CSim 2 a (compositional) rely-guarantee-based framework for the top-down verification of complex concurrent systems in the Isabelle/HOL theorem prover. CSim 2 uses CSimpl, a language with a high degree of expressiveness designed for the specification of concurrent programs. Thanks to its expressibility, CSimpl is able to model many of the features found in real world programming languages like exceptions, assertions, and procedures. CSim 2 provides a framework for the verification of rely-guarantee properties to compositionally reason on CSimpl specifications. Focusing on top-down verification, CSim 2 provides a simulation-based framework for the preservation of CSimpl rely-guarantee properties from specifications to implementations. By using the simulation framework, properties proven on the top layers (abstract specifications) are compositionally propagated down to the lowest layers (source or machine code) in each concurrent component of the system. Finally, we show the usability of CSim 2 by running a case study over two CSimpl specifications of an Arinc-653 communication service. In this case study, we prove a complex property on a specification, and we use CSim 2 to preserve the property on lower abstraction layers.

Sign in / Sign up

Export Citation Format

Share Document