Tim Leinmuller

Hardware Security and trustworthiness are becoming ever more important, especially for security-critical applications like autonomous driving and service robots. With the increase in distribution of RISC-V processors, security issues in them arise. Security vulnerabilities and design flaws in processors can be exploited by attackers, e.g. by running software exploiting the vulnerabilities. This can lead to drastic consequences like damaging whole system functionality and even human lives can be endangered. Hence, it is very important to verify compliance of processors with the design specification and microarchitecture intent to harden the hardware against malicious attacks. Detection and removal of design bugs results in improved processor security. Therefore, we formally verify in this paper the security-critical functionality of a commercial RISC-V processor using model checking based formal verification with the formal verification tool Jasper. For this, we determined and implemented a comprehensive list of properties for security-critical functionality, derived from RISC-V specification and processor microarchitecture intent. The properties cover the security-critical functionality within a RISC-V processor. With our verification experiments, we detected design bugs which have been confirmed by the design team.

The idea behind collective perception is to improve vehicles' awareness about their surroundings. Every vehicle shares information describing its perceived environment by means of V2X communication. Similar to other information shared using V2X communication, collective perception information is potentially safety relevant, which means there is a need to assess the reliability and quality of received information before further processing. Transmitted information may have been forged by attackers or contain inconsistencies e.g. caused by malfunctions. This paper introduces a novel approach for estimating a belief that a pair of entities, e.g. two remote vehicles or the host vehicle and a remote vehicle, within a Vehicular ad hoc Network (VANET) are both trustworthy. The method updates the belief based on the consistency of the data that both entities provide. The evaluation shows that the proposed method is able to identify forged information.

Cooperative Intelligent Transportation Systems (cITS) are a promising technology to enhance driving safety and efficiency. Vehicles communicate wirelessly with other vehicles and infrastructure, thereby creating a highly dynamic and heterogeneously managed ad-hoc network. It is these network properties that make it a challenging task to protect integrity of the data and guarantee its correctness. A major component is the problem that traditional security mechanisms like PKI-based asymmetric cryptography only exclude outsider attackers that do not possess key material. However, because attackers can be insiders within the network (i.e., possess valid key material), this approach cannot detect all possible attacks. In this survey, we present misbehavior detection mechanisms that can detect such insider attacks based on attacker behavior and information analysis. In contrast to well-known intrusion detection for classical IT systems, these misbehavior detection mechanisms analyze information semantics to detect attacks, which aligns better with highly application-tailored communication protocols foreseen for cITS. In our survey, we provide an extensive introduction to the cITS ecosystem and discuss shortcomings of PKI-based security. We derive and discuss a classification for misbehavior detection mechanisms, provide an in-depth overview of seminal papers on the topic, and highlight open issues and possible future research trends.