Gordian: Formal Reasoning Based Outlier Detection for Secure Localization

Matthew Weber, Baihong Jin, Gil Lederman, Yasser Shoukry, Edward A. Lee, Sanjit A. Seshia and Alberto L. Sangiovanni-Vincentelli

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2019-1
January 11, 2019

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2019/EECS-2019-1.pdf

Accurate localization from Cyber-Physical Systems (CPS) is a critical enabling technology for context aware applications and CPS control. As localization plays an increasingly safety-critical role, location systems must be able to identify and eliminate faulty measurements to prevent dangerously inaccurate localization. In this paper we consider the range-based localization problem and propose a method to detect coordinated adversarial corruption on anchor positions and distance measurements. Our algorithm, Gordian, rapidly finds attacks by identifying geometric inconsistencies at the graph level without requiring assumptions about hardware, ranging mechanisms or cryptographic protocols. We give necessary conditions for which attack detection is guaranteed to be successful in the noiseless case, and use that intuition to extend Gordian to the noisy case where fewer guarantees are possible. In simulations generated from real-world sensor noise, we empirically show Gordian’s trilateration counterexample generation procedure enables rapid attack detection even for combinatorially difficult problems.


BibTeX citation:

@techreport{Weber:EECS-2019-1,
    Author = {Weber, Matthew and Jin, Baihong and Lederman, Gil and Shoukry, Yasser and Lee, Edward A. and Seshia, Sanjit A. and Sangiovanni-Vincentelli, Alberto L.},
    Title = {Gordian: Formal Reasoning Based Outlier Detection for Secure Localization},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2019},
    Month = {Jan},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2019/EECS-2019-1.html},
    Number = {UCB/EECS-2019-1},
    Abstract = {Accurate localization from Cyber-Physical Systems (CPS) is a critical enabling technology for context aware applications and CPS
control. As localization plays an increasingly safety-critical role, location systems must be able to identify and eliminate faulty
measurements to prevent dangerously inaccurate localization. In this paper we consider the range-based localization problem and
propose a method to detect coordinated adversarial corruption on anchor positions and distance measurements. Our algorithm,
Gordian, rapidly finds attacks by identifying geometric inconsistencies at the graph level without requiring assumptions about hardware, ranging mechanisms or cryptographic protocols. We give necessary conditions for which attack detection is guaranteed to be successful in the noiseless case, and use that intuition to extend Gordian to the noisy case where fewer guarantees are possible. In simulations generated from real-world sensor noise, we empirically show Gordian’s trilateration counterexample generation procedure enables rapid attack detection even for combinatorially difficult problems.}
}

EndNote citation:

%0 Report
%A Weber, Matthew
%A Jin, Baihong
%A Lederman, Gil
%A Shoukry, Yasser
%A Lee, Edward A.
%A Seshia, Sanjit A.
%A Sangiovanni-Vincentelli, Alberto L.
%T Gordian: Formal Reasoning Based Outlier Detection for Secure Localization
%I EECS Department, University of California, Berkeley
%D 2019
%8 January 11
%@ UCB/EECS-2019-1
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2019/EECS-2019-1.html
%F Weber:EECS-2019-1