Engineering topics

Levitt, Karl

Publications and source records attributed to Levitt, Karl.

3 records

DOE OSTI2015

Security vulnerabilities of connected vehicle streams and their impact on cooperative driving

Autonomous vehicles capable of navigating unpredictable real-world environments with little human feedback are a reality today. Such systems rely heavily on onboard sensors such as cameras, radar/LIDAR, and GPS as well as capabilities such as 3G/4G connectivity and V2V/V2I communication to make real-time maneuvering decisions. Autonomous vehicle control imposes very strict requirements on the security of the communication channels used by the vehicle to exchange information as well as the control logic that performs complex driving tasks such as adapting vehicle velocity or changing lanes. This research presents a first look at the effects of security attacks on the communication channel as well as sensor tampering of a connected vehicle stream equipped to achieve CACC. Our simulation results show that an insider attack can cause significant instability in the CACC vehicle stream. We also outline how different countermeasures, such as downgrading to ACC mode, could potentially be used to improve the security and safety of the connected vehicle streams.

42 ENGINEERING↗

NASA NTRS1993

Formal verification of a microcoded VIPER microprocessor using HOL

The Royal Signals and Radar Establishment (RSRE) and members of the Hardware Verification Group at Cambridge University conducted a joint effort to prove the correspondence between the electronic block model and the top level specification of Viper. Unfortunately, the proof became too complex and unmanageable within the given time and funding constraints, and is thus incomplete as of the date of this report. This report describes an independent attempt to use the HOL (Cambridge Higher Order Logic) mechanical verifier to verify Viper. Deriving from recent results in hardware verification research at UC Davis, the approach has been to redesign the electronic block model to make it microcoded and to structure the proof in a series of decreasingly abstract interpreter levels, the lowest being the electronic block level. The highest level is the RSRE Viper instruction set. Owing to the new approach and some results on the proof of generic interpreters as applied to simple microprocessors, this attempt required an effort approximately an order of magnitude less than the previous one.

Levitt, Karl↗

NASA NTRS1992

Formal mechanization of device interactions with a process algebra

The principle emphasis is to develop a methodology to formally verify correct synchronization communication of devices in a composed hardware system. Previous system integration efforts have focused on vertical integration of one layer on top of another. This task examines 'horizontal' integration of peer devices. To formally reason about communication, we mechanize a process algebra in the Higher Order Logic (HOL) theorem proving system. Using this formalization we show how four types of device interactions can be represented and verified to behave as specified. The report also describes the specification of a system consisting of an AVM-1 microprocessor and a memory management unit which were verified in previous work. A proof of correct communication is presented, and the extensions to the system specification to add a direct memory device are discussed.

Schubert, E. Thomas↗