scholarly journals Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models

2021 ◽  
pp. 303-316
Author(s):  
Alasdair Armstrong ◽  
Brian Campbell ◽  
Ben Simner ◽  
Christopher Pulte ◽  
Peter Sewell
Keyword(s):  
Operating Systems ◽  
Software Verification ◽  
Full Scale ◽  
Hardware Verification ◽  
Instruction Set ◽  
Web Interface ◽  
Instruction Fetch ◽  
Address Translation ◽  
User Instructions ◽  
Relaxed Memory

AbstractArchitecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, either in mathematics or in tools. These ISA semantics can be surprisingly large and intricate, e.g. 100k+ lines for Armv8-A.   In this paper we present a tool, Isla, for computing the allowed behaviours of concurrent litmus tests with respect to full-scale ISA definitions, in Sail, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications, which should be valuable also for other verification tasks. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V.   By using full-scale and authoritative ISA semantics, this lets one evaluate litmus tests using arbitrary user instructions with high confidence. Moreover, because these ISA specifications give detailed and validated definitions of the sequential aspects of systems functionality, as used by hypervisors and operating systems, e.g. instruction fetch, exceptions, and address translation, our tool provides a basis for developing concurrency semantics for these. We demonstrate this for the Armv8-A instruction-fetch model and self-modifying code examples of Simner et al.

scholarly journals ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures

2020 ◽  
pp. 626-655
Author(s):  
Ben Simner ◽  
Shaked Flur ◽  
Christopher Pulte ◽  
Alasdair Armstrong ◽  
Jean Pichon-Pharabod ◽  
...  
Keyword(s):  
Software Verification ◽  
Critical Systems ◽  
Instruction Sets ◽  
Instruction Fetch ◽  
Robust Model ◽  
Address Translation ◽  
Systems Software ◽  
Hardware Implementations ◽  
Observable Behaviour ◽  
Instruction Caches

AbstractComputing relies on architecture specifications to decouple hardware and software development. Historically these have been prose documents, with all the problems that entails, but research over the last ten years has developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets and “user-mode” concurrency, clarifying architectures and bringing them into the scope of programming-language semantics and verification. However, the system semantics, of instruction-fetch and cache maintenance, exceptions and interrupts, and address translation, remains obscure, leaving us without a solid foundation for verification of security-critical systems software.In this paper we establish a robust model for one aspect of system semantics: instruction fetch and cache maintenance for ARMv8-A. Systems code relies on executing instructions that were written by data writes, e.g. in program loading, dynamic linking, JIT compilation, debugging, and OS configuration, but hardware implementations are often highly optimised, e.g. with instruction caches, linefill buffers, out-of-order fetching, branch prediction, and instruction prefetching, which can affect programmer-observable behaviour. It is essential, both for programming and verification, to abstract from such microarchitectural details as much as possible, but no more. We explore the key architecture design questions with a series of examples, discussed in detail with senior Arm staff; capture the architectural intent in operational and axiomatic semantic models, extending previous work on “user-mode” concurrency; make these models executable as test oracles for small examples; and experimentally validate them against hardware behaviour (finding a bug in one hardware device). We thereby bring these subtle issues into the mathematical domain, clarifying the architecture and enabling future work on system software verification.

Comparison of Model Checking Tools

2013 ◽  
Vol 659 ◽  
pp. 181-185
Author(s):  
Wei Gong ◽  
Jun Wei Jia
Keyword(s):  
Model Checking ◽  
Software Verification ◽  
Bounded Model Checking ◽  
Hardware Verification ◽  
Model Checker ◽  
Software And Hardware ◽  
Inherent Part

Model Checking is a method for verification. The model will be checked until the specification of it is proved or disproved. With the rising complexity of big models, there are non-checkable cases, in which cases the problem can be analyzed by some models, for example, bounded Model Checking means to analyze the model until a defined time or depth. The verification happens automatically. The programs for doing this are called Model Checking Tools or Model Checker. Model Checking are used in both software and hardware verification. It is an inherent part of hardware verification, whereas it is less used in the software verification.

scholarly journals Sisyfos: A Modular and Extendable Open Malware Analysis Platform

2021 ◽  
Vol 11 (7) ◽  
pp. 2980
Author(s):  
Dimitrios Serpanos ◽  
Panagiotis Michalopoulos ◽  
Georgios Xenos ◽  
Vasilios Ieronymakis
Keyword(s):  
Feature Extraction ◽  
Operating Systems ◽  
Critical Infrastructure ◽  
Malware Analysis ◽  
Web Interface ◽  
Operational Environment ◽  
Android Malware ◽  
Analysis Platform

Sisyfos is a modular and extensible platform for malware analysis; it addresses multiple operating systems, including critical infrastructure ones. Its purpose is to enable the development and evaluation of new tools as well as the evaluation of malware classifiers. Sisyfos has been developed based on open software for feature extraction and is available as a stand-alone tool with a web interface but can be integrated into an operational environment with a continuous sample feed. We present the structure and implementation of Sisyfos, which accommodates analysis for Windows, Linux and Android malware.

scholarly journals A Basic Microkernel for the RISC-V Instruction Set Architecture

2021 ◽  
Author(s):  
Benjamin William Mezger ◽  
Fabricio Bortoluzzi ◽  
Cesar Albenes Zeferino ◽  
Paulo Roberto Oliveira Valim ◽  
Douglas Rossi Melo
Keyword(s):  
Operating System ◽  
Operating Systems ◽  
System Development ◽  
Abstract Model ◽  
Instruction Set ◽  
Instruction Set Architecture ◽  
Software Application

ABSTRACTComputer processors provide an abstract model known as theinstruction set architecture, which serves as an interface betweenthe available hardware and the software. Application developersneed to communicate with these types of hardware, and having tolearn each computer specification is difficult and time-consuming.Operating systems provide an abstraction towards the availablecomputer hardware and user software. They manage computerresources to enable application programmers to communicate withthe available hardware. This work introduces an academic-orientedoperating system for the RISC-V architecture, a de facto instructionset architecture standard, and compares the solution with othersmall operating systems using the same architecture. As the maincontribution, this work provides an extensible operating system tointroduce students to operating system development.

scholarly journals The SEMAINE API: Towards a Standards-Based Framework for Building Emotion-Oriented Systems

2010 ◽  
Vol 2010 ◽  
pp. 1-21 ◽  
Author(s):  
Marc Schröder
Keyword(s):  
Open Source ◽  
Programming Languages ◽  
Operating Systems ◽  
Research Community ◽  
Full Scale ◽  
Standard Representation ◽  
Message Oriented Middleware ◽  
Open Source Framework ◽  
System Components ◽  
Minimal Effort

This paper presents the SEMAINE API, an open source framework for building emotion-oriented systems. By encouraging and simplifying the use of standard representation formats, the framework aims to contribute to interoperability and reuse of system components in the research community. By providing a Java and C++ wrapper around a message-oriented middleware, the API makes it easy to integrate components running on different operating systems and written in different programming languages. The SEMAINE system 1.0 is presented as an example of a full-scale system built on top of the SEMAINE API. Three small example systems are described in detail to illustrate how integration between existing and new components is realised with minimal effort.

Sign in / Sign up

Export Citation Format

Share Document