Senior Formal Verification Engineer at Apple
Collaborating Professor
Computer Networks Laboratory
Computer Science Department
Federal University of Paraíba
vivek.nigam@gmail.com
» I accepted an offer from Apple to be a Senior Formal Verification Engineer in Munich.
This article proposes automated methods for threat analysis using a model-based engineering methodologythat provides precise guarantees with respect to safety goals. This is accomplished by proposing an intrudermodel for automotive SOA which together with the system architecture and the loss scenarios identified bysafety analysis are used as input for computing assets, impact rating, damage/threat scenarios, and attack paths.To validate the proposed methodology, we developed a faithful model of the autonomous driving functionsof the Apollo framework, a widely used open source autonomous driving stack. The proposed machineryautomatically enumerates several attack paths on Apollo, including attack paths not reported in the literature.
The adoption of autonomous cars requires operational critical functions even in the event of HW faults and/or SWdefects, and protection of safety-critical functions against securitythreats. Defining appropriate safe and secure architectures ischallenging and costly. In previous work, we have proposedtools to automate the recommendation of safety and securitypatterns for safety-critical systems. However, safety and securitymeasures may (negatively) influence system performance, besidesintroducing additional development effort. We present a designspace exploration approach, a model-based engineering workflowand tool prototype for automated guidance on trade-off decisionswhen applying safety and security patterns on a given (unsafe)baseline architecture. Based on models that abstract the vehicle’sfunctionality and its software and hardware components, as wellas an engine for the automated pattern recommendation, weinvestigate the optimization of HW/SW deployments, and providea trade-off analysis for different architecture candidates. Weimplemented our approach in an open-source tool and evaluateit with a model of the Apollo autonomous driving platform.
Software Defined Networking (SDN) is a network paradigm that decouples the network’s control plane, delegated to the SDN controller, from the data plane, delegated to SDN switches.Given the complexity of cyber-physical systems (CPS), such as swarms of drones, often deviations, from a planned mission or protocol, occur which may in some cases lead to harm and losses. To increase the robustness of such systems, it is necessary to detect when deviations happen and diagnose the cause(s) for a deviation. We build on our previous work on soft agents, a formal framework based on using rewriting logic for specifying and reasoning about distributed CPS, to develop methods for diagnosis of CPS at design time. We accomplish this by (1) extending the soft agents framework with Fault Models; (2) proposing a protocol specification language and the definition of protocol deviations; and (3) development of workflows/algorithms for detection and diagnosis of protocol deviations. Our approach is partially inspired by existing work using counterfactual reasoning for fault ascription. We demonstrate our machinery with a collection of experiments.