Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Trustworthy Systems Research

Description

This lecture provides an overview of the trustworthy systems research agenda, highlighting the need for proven trustworthiness in computer systems due to increasing vulnerabilities in embedded systems. The instructor discusses the challenges in verifying complex systems, the concepts of physical and logical isolation, the design decisions behind the SEL4 microkernel, and the rigorous approach to achieving true trustworthiness in critical systems.

Official source

Related concepts (31)

Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Memory management

Memory management is a form of resource management applied to computer memory. The essential requirement of memory management is to provide ways to dynamically allocate portions of memory to programs at their request, and free it for reuse when no longer needed. This is critical to any advanced computer system where more than a single process might be underway at any time. Several methods have been devised that increase the effectiveness of memory management.

Formal methods

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Memory management unit

A memory management unit (MMU), sometimes called paged memory management unit (PMMU), is a computer hardware unit that examines all memory references on the memory bus, translating these requests, known as virtual memory addresses, into physical addresses in main memory. In modern systems, programs generally have addresses that access the theoretical maximum memory of the computer architecture, 32 or 64 bits. The MMU maps the addresses from each program into separate areas in physical memory, which is generally much smaller than the theoretical maximum.

Complexity

Complexity characterises the behaviour of a system or model whose components interact in multiple ways and follow local rules, leading to non-linearity, randomness, collective dynamics, hierarchy, and emergence. The term is generally used to characterize something with many parts where those parts interact with each other in multiple ways, culminating in a higher order of emergence greater than the sum of its parts. The study of these complex linkages at various scales is the main goal of complex systems theory.

Related lectures (32)

Can fish see water?, Design for Sustainability

Explores crafting design interventions for sustainability in different domains.

Transition to Smart Cities: Complexity and Interdependencies MOOC: Smart Cities, Management of Smart Urban Infrastructures

Delves into the complexity and interdependencies of transitioning to smart cities, emphasizing the importance of a holistic approach.

Ariane 501 Case Study

Analyzes the Ariane 501 case study, focusing on the software errors and system complexities that led to a launch failure.

Linear Systems: Convergence and Methods

Explores linear systems, convergence, and solving methods with a focus on CPU time and memory requirements.

Embedded Systems: Introduction