Sampling based Computation of Viability Domain to Prevent Safety Violations by Attackers

Extracted source text ยท arXiv 2110.08632

% \documentclass[preprint]{elsarticle}
% \documentclass[letterpaper, 10pt,journal]{IEEEtran}
% \documentclass[10pt,conference]{IEEEtran}
\documentclass[10pt,conference]{ieeeconf}
% \documentclass[journal,twoside,web]{ieeecolor}
% \usepackage{lineno,hyperref}
% \modulolinenumbers[5]
% \usepackage{generic}
% \usepackage{generic}
\usepackage{textcomp}
% \usepackage{hyperref}       % hyperlinks
\usepackage{url}            % simple URL typesetting
\usepackage{amsfonts}       % blackboard math symbols
\usepackage{xcolor}
\let\proof\relax
\let\endproof\relax
\usepackage{amsmath, amssymb, mathtools, amsthm}
\usepackage{graphicx}
% \usepackage{algorithm, algorithmic}
\usepackage{bm}
\usepackage{float}
\usepackage{color}
\usepackage{epstopdf}
\usepackage[ruled,vlined,linesnumbered,noend]{algorithm2e}
\newcommand{\alvaro}[1]{\textcolor{blue}{\sf #1}}


\makeatletter
\let\NAT@parse\undefined
\makeatother


\usepackage{hyperref}
\makeatletter
\hypersetup{colorlinks=true}
\AtBeginDocument{\@ifpackageloaded{hyperref}
  {
  \def\@linkcolor{blue}
  \def\@anchorcolor{red}
  \def\@citecolor{red}
  \def\@filecolor{red}
  \def\@urlcolor{black}
  \def\@menucolor{red}
  \def\@pagecolor{red}
\begingroup
  \@makeother\`%
  \@makeother\=%
  \edef\x{%
    \edef\noexpand\x{%
      \endgroup
      \noexpand\toks@{%
        \catcode 96=\noexpand\the\catcode`\noexpand\`\relax
        \catcode 61=\noexpand\the\catcode`\noexpand\=\relax
      }%
    }%
    \noexpand\x
  }%
\x
\@makeother\`
\@makeother\=
}{}}
\makeatother

\renewcommand\qedsymbol{$\blacksquare$}


\newtheorem{Theorem}{Theorem}
% \newtheorem{Theorem}[FTS]{Theorem}
% \newtheorem{Theorem}[FTS]{Theorem}
% \newtheorem{Theorem}[FTS]{Theorem}
% \newtheorem{Theorem}[FTS]{Theorem}
% \newtheorem{Theorem}[FTS]{Theorem}
% \newtheorem{FTS 4-1}[FTS]{Theorem}
% \newtheorem{Theorem}[FTS]{Theorem}
% \newtheorem{Theorem}[FTS]{Theorem}

\newtheorem{Lemma}{Lemma}

\newtheorem{Problem}{Problem}

\newtheorem*{Problem*}{Problem}

\newtheorem{Remark}{Remark}

\newtheorem{Proposition}{Proposition}

\newtheorem{Corollary}{Corollary}

\newtheorem{Example}{Example}

\newtheorem{Assumption}{Assumption}

\newtheorem{Definition}{Definition}

% \renewcommand{\baselinestretch}{0.91}

\IEEEoverridecommandlockouts
% \pagestyle{empty}

\def\BibTeX{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em
    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}

\begin{document}

% \title{\LARGE{\bf Secure by Design: Finding Bounds to Prevent Damages from Attacks}}

\title{\LARGE{\bf Sampling based Computation of Viability Domain to \\ Prevent Safety Violations by Attackers}}

\author{Kunal~Garg \and
% \IEEEmembership{Student Member, IEEE}, 
Alvaro~A.~Cardenas \and Ricardo~G.~Sanfelice
% \IEEEmembership{Senior Member, IEEE}
\thanks{
The research was sponsored by the Army Research Office and was accomplished under Grant Number W911NF-20-1-0253. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Army Research Office or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes, notwithstanding any copyright notation herein.
% This paragraph of the first footnote will contain the date on which you submitted your brief for review. It will also contain support information, including sponsor and financial support acknowledgment. For  example, ``This work was supported in part by the U.S. Department of  Commerce under Grant BS123456.'' 
}
}
\maketitle
% \thispagestyle{empty}
\begin{abstract}
This paper studies the security of cyber-physical systems under attacks. Our goal is to design system parameters, such as a set of initial conditions and input bounds so that it is secure by design. To this end, we propose new sufficient conditions to guarantee the safety of a system under adversarial actuator attacks. Using these conditions, we propose a computationally efficient sampling-based method to verify whether a set is a viability domain for a general class of nonlinear systems. In particular, we devise a method of checking a modified barrier function condition on a finite set of points to assess whether a set can be rendered forward invariant. Then, we propose an iterative algorithm to compute the set of initial conditions and input constraint set to limit what an adversary can do if it compromises the vulnerable inputs. Finally, we utilize a Quadratic Program approach for online control synthesis. 
\end{abstract}

% \begin{IEEEkeywords}
% Distributed algorithms, Optimization, Nonlinear control systems,  Power generation dispatch
% \end{IEEEkeywords}

\section{Introduction}
Security has become one of the most critical problems in the field of Cyber-Physical Systems (CPS), as illustrated by several incidents of attacks that happened in the past few years~\cite{lee2014german,oueslati2019comparative}. There are two types of security mechanisms for protecting CPS~\cite{cardenascyber} i) proactive, which considers design choices deployed in the CPS \emph{before} attacks, and ii) reactive, which take effect after an attack is detected.%, and they reconfigure the system online to minimize the impact of the attack. 
%For safe and reliable operations of CPS, it is essential that the designed control strategies are resilient against various possible attacks, such as attacks on the system's sensors, actuators, communication systems, or decision-making modules.   

%As discussed in \cite{cardenascyber}, there are two ways of mitigating attacks, i) proactive, which considers design choices deployed in the CPS before any attack, and ii) reactive, which take effect once an attack has been detected and they reconfigure the system online in order to minimize the impact of the attack. 
While reactive methods are less conservative than proactive mechanisms, they heavily rely on fast and accurate attack detection mechanisms. 
%On the other hand, proactive methods, such as designing the system, though conservatively, do not rely on such additional mechanisms. 
Although there is a plethora of work on attack detection for CPS~\cite{choi2018detecting,renganathan2020distributionally},  it is generally possible to design a stealthy attack such that the system behavior remains close to its expected behavior, thus evading attack-detection solutions~\cite{urbina2016limiting}. Intrusion detection systems also produce a large number of false positives, which can lead to a large operational overhead of security analysts dealing with irrelevant alerts~\cite{cardenas2006framework}. On the other hand, a proactive method can be more effective in practice, particularly against stealthy attacks. 
%might become a significant operational nuisance during normal operations. %Finally, as argued in \cite{wu2021secure}, reactive schemes have limited broader applications since an attacker can monitor and acquire the knowledge of the system's defense mechanisms and launch an effective attack.   
Attacks on a CPS can disrupt the natural operation of the system. 
% Among other desirable properties of a control system,
One of the most desirable system properties is \textit{safety}, i.e., the system does not go out of a safe zone. Safety is an essential requirement, violation of which can result in failure of the system, loss of money, or even loss of human life, particularly when a system is under attack \cite{al2018cyber}.

In most practical problems, safety can be realized as guaranteeing forward-invariance of a safe set. Control barrier function (CBF) based approach \cite{ames2017control} to guarantee forward invariance of the safe region has become very popular in the last few years since a safe control input can be efficiently computed using a Quadratic Program (QP) with CBF condition as the constraint. Most of the prior work on safety using CBFs, e.g., \cite{ames2017control}, assumes that the \textit{viability} domain, i.e., the set of initial conditions from which forward invariance of the safe set can be guaranteed, is known. In practice, it is not an easy task to compute the viability domain for a nonlinear control system. Optimization-based methods, such as Sum-of-Squares (SOS) techniques, have been used in the past to compute this domain (see \cite{wang2018permissive}). However, SOS-based approaches are only applicable to systems whose dynamics is given by polynomial functions, thus limiting their applications. Another method popularly used in the literature for computing the viability domain is Hamilton-Jacobi (HJ) based reachability analysis, see, e.g., \cite{choi2021robust}. However, such an analysis is computationally expensive, particularly for higher dimensional systems. We propose a novel sampling-based method to compute the viability domain for a general class of nonlinear control systems to overcome these limitations.

% In this paper, we propose a proactive method for designing a system resilient to actuator attacks.
In this work, we consider a general class of nonlinear systems under actuator attacks and propose a method of computing a set of initial conditions and an input constraint set such that the system remains \textit{secure by design}. In particular, we consider actuator manipulation, where an attacker can assign arbitrary values to the input signals for a subset of the actuators in a given bound. We consider the property of safety with respect to an unsafe set and propose sufficient conditions using sampling of the boundary of a set to verify whether the set is a \textit{viability domain} under attacks. Using these conditions, we propose a computationally tractable algorithm to compute the set of initial conditions and the input constraint set such that the system's safety can be guaranteed under attacks. In effect, our proposed method results in a secure-by-design system that is resilient against actuator attacks. Finally, we leverage these sets in a QP-based approach with provable feasibility for real-time online feedback synthesis. The contributions of the paper are summarized below:
\begin{itemize}
    % \item[1)] In contrast to most of the prior work on security, where forward reachability is used for safety, we utilize CBFs to derive sufficient conditions for safety under a class of attacks on system inputs;
    \item[1)] We present sampling-based sufficient conditions to assess whether a given set can be rendered forward invariant for a general class of nonlinear system. To the best of the authors' knowledge, this is the first work utilizing sampled-data approach for computing a viability domain;
    \item[2)] We present a novel iterative algorithm to compute a viability domain and an input constraint set to guarantee system safety under attacks. Unlike \cite{wang2018permissive,choi2021robust}, the proposed method is applicable for general nonlinear control systems and is scalable with the system dimension.
\end{itemize}

\noindent \textit{Notation}: Throughout the paper, $\mathbb R$ denotes the set of real numbers and $\mathbb R_+$ denotes the set of non-negative real numbers. We use $|x|$ to denote the Euclidean norm of a vector $x\in \mathbb R^n$. We use $\partial S$ to denote the boundary of a closed set $S\subset \mathbb R^n$ and $\textrm{int}(S)$ to denote its interior and $|x|_S = \inf_{y\in S}|x-y|$, to denote the distance of $x\in \mathbb R^n$ from the set $S$. The Lie derivative of a continuously differentiable function $h:\mathbb R^n\rightarrow\mathbb R$ along a vector field $f:\mathbb R^n\rightarrow\mathbb R^m$ at a point $x\in \mathbb R^n$ is denoted as $L_fh(x) \coloneqq \frac{\partial h}{\partial x}(x)f(x)$. 
% A continuous function $\alpha:\mathbb R_+\rightarrow\mathbb R_+$ is said to belong to class$-\mathcal K$ if it is monotonically increasing with $\alpha(0) = 0$. 
% We use $\mathbb B_\epsilon$ to denote a ball of radius $\epsilon>0$ centered at the origin. 
% Let $d_S(x,y)$ denote the  between points $x,y\in \partial S$ along the boundary of a connected set $S$. 


\section{Problem formulation}\label{sec: math prelim}
% \subsection{Notation and Definition}
%We denote by $\dot x(t) = \frac{\text{d}x(t)}{\dt}$ the time derivative of function $x(t)$ and by $y'(s) = \frac{\text{d}y(s)}{\ds}$ the derivative of $y(s)$ with respect to the stretched time $s$.
% We use a standard notation throughout this paper. Specifically,
% \subsection{Notation}
% Given $x\in \mathbb R^n$ and $y\in \mathbb R^m$, $(x,y) \coloneqq [x^T, y^T]^T$. 
We start with defining a model for the system and the attacker considered in this paper. 
% Then, we present the problem formulation and an outline of our approach for solving it.   

\subsection{System model}
Consider a nonlinear control system $\mathcal S$ given as
\begin{align}\label{eq: actual system}
% \hspace{-40pt}\text{\textit{Actual system}:} &   \hspace{30pt} \dot x = \Phi(t,x,u), \quad x(0) = x_0,
\mathcal S : \begin{cases}\dot x = F(x,u) + d(t,x),\\
x\in \mathcal D, u\in \mathcal U,\end{cases}
\end{align}
where $F:\mathcal D\times\mathcal U\to \mathbb R^n$ is a known function continuous on $:\mathcal D\times\mathcal U$, with $\mathcal D\subset\mathbb R^n$ and $\mathcal U\subset \mathbb R^m$, $d:\mathbb R_+\times\mathbb R^n\rightarrow\mathbb R^n$ is unknown and represents the unmodeled dynamics, $x\in \mathcal D$ is the system state, and $u\in \mathcal U$ is the control input. 
% Since the unmodeled dynamics $d$ is unknown, we work with the following model for the system
% \begin{align}\label{eq: model}
% \dot x = F(x,u). 
% \end{align}
\subsection{Attacker model}
In this paper, we consider attacks on the control input of the system. In particular, we consider an attack where a subset of the components of the control input is compromised. Under such an attack, the system input takes the form:
\begin{align}\label{eq: attack model}
   u = (u_v, u_s),
\end{align}
where $u_v\in \mathcal U_v\subset \mathbb R^{m_v}$ represents the \textit{vulnerable} components of the control input that might be compromised or attacked, and $u_s\in \mathcal U_s\subset \mathbb R^{m_s}$ the \textit{secure} part that cannot be attacked, with $m_v + m_s = m$ and $\mathcal U\coloneqq \mathcal U_v\times \mathcal U_s$.
Under this class of attack, we assume that we know which components of the control input are vulnerable. For example, if the system has four inputs so that $u = \begin{bmatrix}u_1& u_2& u_3& u_4\end{bmatrix}^T$, and $u_1, u_3$ can be attacked, then we assume that this information is known, and $u_v$ is comprised of $u_1$ and $u_3$. We discuss how to address the assumption of which components of the control input are vulnerable in Remark \ref{rem: attack model 1} in Section \ref{sec: num method}. 
% We assume that under this class of attacks, the control input constraint set is given as $\mathcal U \coloneqq \begin{bmatrix}\mathcal U_v\\ \mathcal U_s\end{bmatrix}\subset \mathbb R^m$ $u_v$, so that $u_v\in \mathcal U_v$ and $u_s\in \mathcal U_s$.

% 2) \textit{Additive bias}: 
% Note that the attack model \eqref{eq: attack model} also capture an attack where an additive bias is introduced in the control command. Under such an attack, the system input takes the following form:
% \begin{align}\label{eq: attack model additive attack}
%     u = u_{nom} + \tilde u_v,
% \end{align}
% where $u_{nom} = (u_{nom,a}, u_s)$ is the nominal control input and $\tilde u_v$ is the attack vector with $\tilde u_v = (u_v-u_{nom,a}, 0)$ so that the resulting input is $u = (u_v, u_s)$. 

% Under this class of attack, we assume that the set $\tilde {\mathcal U}_v$ represents a fraction of the input constraint set $\mathcal U$. For example, consider a case of a 1-D system with $\mathcal U = \{u\;| \; |u|\leq u_M\}$ for some $u_M>0$. In this case, $\tilde{ \mathcal U}_v$ can be considered to be of the form $\tilde {\mathcal U}_v = \{u \; |\; |u|\leq pu_M\}$ for some $0<p<1$. This attack model represents the scenario where an attacker can manipulate the actuators up to a fraction of their limits. 

Such attack models have been used in prior work, see e.g., \cite{giraldo2020daria}, and can be implemented in practice by designing the dynamic range of the actuator to preserve its bounds. It can also be implemented in software with the help of a reference monitor~\cite{erlingsson2004inlined} between the controller and the actuator that can check if the desired control inputs satisfy the security policy~\cite{giraldo2020daria}. As discussed in \cite{pasqualetti2013attack}, various prototypical attacks, such as \textit{stealth attacks}, \textit{replay attacks}, and \textit{false-data injection attacks} can be captured by the attack model in \eqref{eq: attack model}. In addition to representing a real-world scenario where system actuators have physical limits, constraining the vulnerable control input $u_v$ in the set $\mathcal U_v$ has several advantages:
\begin{itemize}
    \item[1)] It restricts how much an attacker can change the nominal operation of the system \cite{kafash2018constraining}, and can be implemented physically, so an attacker cannot bypass it.
    \item[2)] It can be utilized to design a detection mechanism, e.g., if $u_v\notin \mathcal U_v$, a flag can be raised signifying that the system is under an attack. Schemes that raise a threshold-based flag are commonly used as detection mechanism \cite{renganathan2020distributionally}. 
    % Ideally, an attacker will try to inject undetectable signals. 
    % and so, it injects an attack input that satisfies $u_v\in \mathcal U_v$. 
    \item[3)] The constraint set $\mathcal U_v$ can be designed appropriately such that the system remains \textit{secured} under attacks, as discussed in Section \ref{sec: num method} (see also \cite{giraldo2020daria,kafash2018constraining}). 
\end{itemize}

\begin{figure}[t]
	\centering
	\includegraphics[width=0.8\columnwidth,clip]{overview_figure.png}
	\caption{Overview of our approach.}
	\label{fig:overview}
\end{figure}

Now, we present the control design objectives. Consider a non-empty, compact set $S\subset\mathbb R^n$, referred to as safe set, to be rendered forward invariant. We make the following assumption on the unmodeled dynamics $d$ in \eqref{eq: actual system}:
\begin{Assumption}\label{assum: d bound}
There exists $\delta>0$ such that $|d(t, x)|\leq \delta$ for all $t\geq 0$ and $x\in \mathcal D$.
\end{Assumption}
\noindent We consider two properties when designing the control law, an \textit{essential property (safety)}, imposed while designing the secure input $u_s$, and a \textit{desirable property (performance)}, imposed while designing both $u_s$ and $u_v$ (see Figure \ref{fig:overview}). The problem we study in this paper is as follows. 

\begin{Problem}\label{Problem 1}
Given the system in \eqref{eq: actual system} with unmodeled dynamics $d$ that satisfies Assumption \ref{assum: d bound}, a set $S$ and the attack model in \eqref{eq: attack model}, design a feedback law $k_s:\mathbb R^n\rightarrow \mathcal U_s$, and find a set of initial conditions $X_0\subset S$ and the input constraint set $\tilde{\mathcal U}_v\subset\mathcal U_v$, such that for all $x(0)\in X_0$ and $u_v:\mathbb R_+\rightarrow  \tilde{\mathcal U}_v$, the closed-loop trajectories $x:\mathbb R_+\rightarrow\mathbb R^n$ of \eqref{eq: actual system} resulting from using $u_s = k_s(x)$ satisfy  $x(t) \in S$ for all $t\geq 0$.
\end{Problem}

In plain words, we consider the problem of designing a feedback law $u_s$ and compute a set of initial conditions $X_0$ and input constraint set $\tilde{\mathcal U}_v$, such that even under an attack as per the attack model \eqref{eq: attack model}, the system trajectories do not leave the safe set $S$, i.e., the system is secure by design.
% the safety is guaranteed under the attack model \eqref{eq: attack model}. To this end, we propose a method of choosing the input constraint set $\mathcal U_v$ such that the system remains safe for any attack signal $u_v:\mathbb R_+\rightarrow\tilde{\mathcal U}_v$, and thus, the system is secure by design. 
In this work, we assume that the safe set is given as $S \coloneqq \{x\; |\; B(x)\leq 0\}$ where $B:\mathbb R^n\rightarrow\mathbb R$ is a sufficiently smooth user-defined function.
% Moreover, let $h_{G}:\mathbb R^n\rightarrow\mathbb R$ a continuously differentiable function defining the goal set $S_{G} = \{x\; |\; h_{G}(x)\leq 0\}$. 
% We assume that the interior of the safe sets, $\textrm{int}(S_{S}) = \{x\; |\; h_{S}(x)<0\}$, is non-empty. 
% The problem formulation follows. 
% \begin{Problem}\label{Problem: multiagent ST}
% Find a control input $u(t)\in \mathcal U =\{v\in \mathbb R^m \; |\; u_{j,min}\leq v\leq u_{j,max}, j = 1, 2, \ldots, m\}$, $t\geq 0$, and a set $D$, such that for all $x(0)\in D\subset S_{S}$, the closed-loop trajectories of \eqref{eq: attack model} satisfy
% \begin{itemize}
%     \item[(i)] 
%     % Convergence to the goal set within user-defined time: 
%     $x(\bar T)\in S_{G}$ for some user-defined $\bar T>0$;
%     \item[(ii)] 
%     % Forward invariance of the static safe set: 
%     $x(t)\in S$ for all $t\geq 0$;
%     % \item[(iii)]
%     % % Forward invariance of the time-varying safe set:
%     % $x(t)\in S_{T}$ for all $t\geq 0$.
% \end{itemize}
% \end{Problem}
% where {\small
% \begin{align*}
%  A_u =\begin{bmatrix}1 & 0 & \cdots & 0\\ -1 & 0 & \cdots & 0 \\ 0 & 1 & \cdots & 0\\ 0 & -1 & \cdots & 0\\ & & \vdots & \end{bmatrix} \in \mathbb R^{2m\times m},   b_u = \begin{bmatrix}u_{1,max}\\ -u_{1,min}\\ u_{2,max}\\ -u_{2,min}\\ \vdots\end{bmatrix}\in \mathbb R^{2m}.  
% \end{align*}}\normalsize
% \noindent Thus, we seek a feedback control input $u(t) = u(\hat x(t))$ that solves Problem \ref{Problem: multiagent ST}. 
% {Since the actual states $x$ is not available, it is important to establish relationship between set membership of the actual state $x$ and the estimated state $\hat x$ for any given set $S\subset \mathbb R^n$. Under Assumption \ref{assum hat x eps}, it can be easily shown that for any $t\geq 0$,
% \begin{itemize}
%     \item(i) $x(t)\in S-\mathbb B_\epsilon \implies \hat x(t)\in S$;
%     \item(ii) $\hat x(t)\in S-\mathbb B_\epsilon \implies x(t)\in S$.
% \end{itemize}
% Property (i) will be used to relate the set of estimated states $\{\hat x(0)\}$ with that of the actual states $\{x(0)\}$ (e.g., for computing the admissible set of initial conditions for safety) and property (ii) will be used to relate the set $\{x(t)\}$ with $\{\hat x(t)\}$ at any future time (e.g., to establish the convergence of the system to the goal set). 
% }

\subsection{Outline of approach}
Given a control system \eqref{eq: actual system}, and an attack model \eqref{eq: attack model}, we first identify a safe set $S\subset \mathbb R^n$ and the vulnerable input $u_v$. Then, our approach to solving Problem \ref{Problem 1} involves the following steps (see Figure \ref{fig:overview 2}):
\begin{itemize}
    \item[1)] \textit{Establish the existence of $X_0$ and $\mathcal U_v$ (Section \ref{sec: safety})}: leverage CBFs to find sufficient conditions to check whether there exist a set of initial conditions $X_0$, input constraint set $\tilde{\mathcal U}_v\subset\mathcal U_v$, and a control input $u_s$ for all $x\in X_0$ that can solve Problem \ref{Problem 1};
    \item[2)] \textit{Numerical method for computation of $X_0$ and $\mathcal U_v$ (Section \ref{sec: num method})}: use conditions in step 1) to formulate a numerical method for computing sets $X_0$ and $\tilde{\mathcal U}_v$;
    \item[3)] \textit{Feedback law synthesis (Section \ref{sec: QP control})}: use the sets $X_0$ and $\tilde{\mathcal U}_v$ from step 2) to design a feedback control law $u_s = k_s(x)$ that solves Problem \ref{Problem 1}.
\end{itemize}


\begin{figure}[t]
	\centering
	\includegraphics[width=\columnwidth,clip]{overview_figure_2.png}
	\caption{Approach for safe feedback design under attacks.}
	\label{fig:overview 2}
\end{figure}

\subsection{Preliminaries}
Next, we present preliminaries on forward invariance. 
\begin{Definition}
   A set $S\subset\mathbb R^n$ is termed as \textnormal{forward invariant} for system \eqref{eq: actual system} if every solution $x:\mathbb R_+\rightarrow\mathbb R^n$ of \eqref{eq: actual system} satisfies $x(t)\in S$ for all $t\geq 0$ and for all initial conditions $x(0)\in S$. 
\end{Definition}
Next, we review a sufficient condition for guaranteeing forward invariance of a set in the absence of an attack. For the sake of simplicity, in what follows, we assume that every solution of \eqref{eq: actual system} exists and is unique in forward time for all $t\geq 0$ whether or not there is an attack on the system.\footnote{In this work, we assume that even under attack, the solution of the system is unique in forward time. It is possible to study the case when this assumption does not hold using the notion of strong invariance (see \cite{clarke2008nonsmooth}).} 

\begin{Lemma}[\cite{blanchini1999set}]\label{lemma: nec suff safety d 0}
% Let every solution of \eqref{eq: actual system} exist and be unique in forward time. Then, 
Given a continuously differentiable function $B:\mathbb R^n\rightarrow\mathbb R$, the set $S = \{x\; |\; B(x)\leq 0\}$ is forward invariant for \eqref{eq: actual system} with $d\equiv 0$ if the following condition holds:
\begin{equation}\label{eq: safety cond d 0}
    % \inf_{u\in \mathcal U}\left\{L_{f}h(x)+L_{g}h(x)u\right\}\leq \alpha(-h(x)),
    \inf_{u\in \mathcal U}L_{F}B(x,u)\leq 0 \quad \forall x\in \partial S.
\end{equation}
% Furthermore, if $h(x(0))<0$, then for any $T\geq 0$, $h(x(t))<0$ for all $0\leq t\leq T$. 
\end{Lemma}

Satisfaction of \eqref{eq: safety cond d 0} means the set $S$ is termed as a \textit{viability} domain for system \eqref{eq: actual system} with $d\equiv 0$. Using Lemma \ref{lemma: nec suff safety d 0}, and following the notion of robust CBF in \cite{garg2021robust}, we can state the following result guaranteeing forward invariance in the presence of disturbance $d$.

\begin{Lemma}[\cite{garg2021robust}]\label{lemma: nec suff safety}
% Let every solution of \eqref{eq: actual system} exist and be unique in forward time. Then, 
Given a continuously differentiable function $B:\mathbb R^n\rightarrow\mathbb R$, the set $S = \{x\; |\; B(x)\leq 0\}$ is forward invariant for \eqref{eq: actual system} under $d$ satisfying Assumption \ref{assum: d bound} if the following condition holds:
\begin{equation}\label{eq: safety cond}
    % \inf_{u\in \mathcal U}\left\{L_{f}h(x)+L_{g}h(x)u\right\}\leq \alpha(-h(x)),
    \inf_{u\in \mathcal U}L_{F}B(x,u)\leq -l_B\delta \quad \forall x\in \partial S,
\end{equation}
where $l_B$ is the Lipschitz constant of the function $B$.
% Furthermore, if $h(x(0))<0$, then for any $T\geq 0$, $h(x(t))<0$ for all $0\leq t\leq T$. 
\end{Lemma}

% \noindent A function that satisfies \eqref{eq: safety cond} is called a valid CBF by the authors in \cite{lindemann2019control}, and a zeroing-CBF by the authors in \cite{ames2017control}. 


% \subsection{Fixed-time convergence}
% \subsection{Fixed-time stability} 
% Based on the notion of fixed-time stability of an equilibrium point \cite{polyakov2012nonlinear}, we define the notion of fixed-time stability of a set. A set $G\subset\mathbb R^n$ is called fixed-time stable for the system \eqref{eq: actual system} if 
% \begin{itemize}
%     \item[1)] \textit{Lyapunov stability}: for every $\epsilon>0$, there exists $\delta>0$ such that $|x(0)|_G<\epsilon$ implies $|x(t)|_G<\delta$ for all $t\geq 0$, and
%     \item[2)] \textit{Fixed-time convergence}: there exist a neighborhood $D$ of the set $G$ and a fixed-time $T \in [0,\infty)$ such that for each initial condition $x(0)\in D$ to \eqref{eq: actual system}, the solution $t \mapsto x(t)$ satisfies $x(t) \in G$ for all $t \geq T$.
% \end{itemize}
% % Assuming that the origin is an equilibrium point for a dynamical system, it is called fixed-time stable if it is Lyapunov stable and there exists a fixed time $0<T<\infty$, independent of the initial conditions, such that $x(T) = 0$ for all initial conditions $x(0)$ \cite{polyakov2012nonlinear}.

% We review a sufficient condition for fixed-time stability in the absence of an attack.
% \begin{Lemma}[\hspace{-0.3pt}\cite{garg2021FxTSDomain}]\label{lemma: FxTS new}
% % Let every solution of \eqref{eq: actual system} with $d\equiv 0$ exist and be unique in forward time. 
% Let $G = \{x\; |\; V(x)\leq 0\}$ where $V:\mathbb R^n\rightarrow \mathbb R$ be a continuously differentiable function and assume that there exists $\alpha_1, \alpha_2\in \mathcal K$ such that $\alpha_1(|x|_G)\leq V(x)\leq \alpha_2(|x|_G)$. If the following holds
% \begin{align}\label{eq: dot V ineq new}
%      \inf_{u\in \mathcal U} L_{F}V(x,u) & \leq -\alpha V(x)^{\gamma_1} -\alpha V(x)^{\gamma_2}+\delta_1 V(x),
% \end{align}
% for all $x\notin G$, with $\alpha>0$, $\delta_1\in \mathbb R$, $\gamma_1 = 1+\frac{1}{\mu}$, $\gamma_2 = 1-\frac{1}{\mu}$ for some $\mu>1$. Then, there exists a neighborhood $D$ of the set $G$ such that for all $x(0)\in D $, the trajectories of \eqref{eq: actual system} with $d\equiv 0$ reach the set $G$ in a fixed time $T$ where $T, D$ are functions of $\mu$ and $\frac{\delta_1}{2\alpha}$.
% \end{Lemma}
% The function $V$ can be replaced with $V$ in \eqref{eq: dot V ineq new} so that the above result holds for the set $K$ instead of the origin. 

% \section{Notion of Security}\label{sec: security}
% We first start with the definition of a \textit{secure} system for safety, as required in Problem \ref{Problem 1}. Then, we present sufficient conditions guaranteeing the security of the system under an attack.

% \subsection{Secure system}\label{sec: security def}
% First, we discuss the notion of security in terms of satisfaction of certain desirable properties by the system under an attack. We use $\mathcal S\models P$ to denote that a system $\mathcal S$ in \eqref{eq: actual system} satisfies a property $P$. Based on Problem \ref{Problem 1}, in this paper, we consider safety property (denoted as $P_{safe,S}$), which is satisfied if the system trajectories starting from $S$ evolve in the safe set $S$ for all times.
%     % \item \textbf{Stability} (denoted as $P_{stab}$): the system trajectories remain in a small neighborhood around an equilibrium point or a reference trajectory; or
%     % \item \textit{Fixed-time Convergence} (denoted as $P_{conv,D}$): the system trajectories converge to the goal point or a set, $G$ within the user-defined time $T_{ud}>0$ for all initial conditions $x(0)\in D$.
% % \end{itemize}
% % Thus, $\mathcal S\models P_{safe}$ implies that there exists a feedback law $k$ such that under the effect of the control input $u = k(x)$, the set $S$ is forward invariant for the resulting closed-loop trajectories of the system \eqref{eq: actual system}. 
% A system under the effect of an attack $\mathcal A_{\tau}$, as given by the attacker model \eqref{eq: attack model}, starting at time $t = \tau$ is denoted as $[\mathcal A_\tau]\mathcal S$. Using this notation, we can define the notion of \textit{secured} system as follows.
% % In this paper, we are concerned about attacks on the  Types of attack include:
% % \begin{itemize}
% %     \item \textbf{Sensor Attack} (denoted as $\mathcal A_{I,sens}$): where a subset of the sensor is vulnerable and the output of these sensors $y_a$ takes arbitrary values in the set $\mathcal Y_a$; and
% %     \item \textbf{Input Attack} (denoted as $\mathcal A_{I,inp}$): where a subset of the control actuators are vulnerable and the resulting input $u_v$ takes arbitrary values in the set $\mathcal U_v$. 
% % \end{itemize}

% \begin{Definition}\label{def: robust safety input T}
%   The system $\mathcal S$ in \eqref{eq: actual system} is \textnormal{secure} for a property $P$ at $\tau>0$ under attack $\mathcal A_{\tau}$ and \eqref{eq: attack model} if $[\mathcal A_\tau]\mathcal S\models P$.
% \end{Definition}

% % \begin{Assumption}\label{assum hs ht L}
% % There exist $l_S, l_G>0$ such that $\left |\frac{\partial h_{S}}{\partial x}(x)\right| \leq l_S, \left |\frac{\partial h_{G}}{\partial x}(x)\right| \leq l_G $,
% % for all $x\in \mathcal D\subset \mathbb R^n$, and all $t\geq 0$.
% % \end{Assumption}

% % \noindent Since the functions $h_{S}, h_{G}$ are continuously differentiable, Assumption \ref{assum hs ht L} can be easily satisfied in any compact domain $\mathcal D$.

% In particular, the system \eqref{eq: actual system} is \textit{secure with respect to the safety property $P_{safe,S}$} for the safe set $S$ if for all initial conditions $x(0)\in S$,  $x(t)\in S$ for all $t\geq 0$, $u_v\in \mathcal U_v$ and $d$ satisfying Assumption \ref{assum: d bound}.
% % More formally, we define the notion of \textit{vulnerable} system as follows:
% % \begin{Definition}\label{def: safety secured}
% In other words, for the safety property $P_{safe,S}$, an attack on the system \eqref{eq: actual system} is successful if an attack signal $u_v:\mathbb R_+\to \mathcal U_v$ can drive a system trajectory, starting in the set $S$, out of the safe set $S$. 
% % at point $x_a\in \partial S$  if there exist an open neighbor hood $\mathcal N_a$ of $x_a$ and an attack signal $u_v(x)\in \mathcal U_v$ such that
% % \begin{align}\label{eq: attack def}
% %     % \inf_{u_s\in \mathcal U_s}\{L_fB(x) + L_{g_s}B(x)u_s\} > -L_{g_v}h_{S}(x_a)u_v(x).
% %     \inf_{u_s\in \mathcal U_s}L_F B(x,u_v(x),u_s)>0, \quad \forall x\in \mathcal N_a\cap S.
% % \end{align}
% % Furthermore, the system is termed as \textnormal{globally vulnerable} if the above holds for all $x_a\in \partial S$. 
% % \end{Definition}

% % \noindent It is easy to see that the system is invulnerable with respect to the safety property if and only if it is secured for the safety property. In other words, the system is secured with respect to the safety property if and only if \eqref{eq: attack def} does not hold for any $x_a\in \partial S$. 

% % Similarly, the notion of security for the convergence property can be defined as follows. 
% % Let $D_G\supset K$ denote the domain of fixed-time stability of the set $K$ for a given time $T_{ud}$, given as $D_G = \{x(0) \in \mathbb R^n \; |\; \lim\limits_{t\to T_{ud}} x(t)\in K\}$. 
% % An estimate of the domain of attraction is computed as the largest sublevel set of the function $V$ where its time derivative takes negative values. 
% % We say that an attack on the system \eqref{eq: actual system} is successful if the attack vector $u_v$ is able to prevent the system trajectories from reaching the set $G$ in the required time $T_{ud}$. 
% % More formally, we define the notion of \textit{vulnerable} system as follows:
% % \begin{Definition}
% % Thus, the system \eqref{eq: actual system} is \textit{secure with respect to the convergence property $P_{conv,D}$} for the goal set $G$ if there exists a neighborhood $D$ of the set $G$ such that for all $x(0)\in D$, it holds that $x(T_{ud})\in G$. 
% % of $x_a$ and an attack signal $u_v(x)\in \mathcal U_v$ such that
% % \begin{align}\label{eq: attack def conv}
% %     % \inf_{u_s\in \mathcal U_s}\{L_fV(x) + L_{g_s}V(x)u_s\} > -L_{g_v}h_{G}(x_a)u_v(x).
% %     \hspace{-10pt}\inf_{u_s\in \mathcal U_s}\{L_F h_{G}(x_a,u_v(x), u_s) > 0, \; \forall x\in \mathcal N_a\cap \partial D_G.
% % \end{align}
% % Furthermore, the system is termed as \textnormal{globally vulnerable with respect to the convergence property $P_{conv}$} if the above holds for all $x_a\in \partial D_G$. 
% % \end{Definition}

% Next, we present sufficient conditions that guarantee the security of the system model \eqref{eq: actual system} against attacks on the input.

% % \subsection{Robust CBF and CLF}
% % \noindent \textbf{Robust CBF and CLF}: First, we present conditions for robust CBFs so that the safety requirements (ii) and (iii) in Problem \ref{Problem: multiagent ST} can be satisfied in the presence of the disturbance $d$ and error $\epsilon$. We make the following assumption. 

\section{Sufficient conditions for safety}\label{sec: safety}
In this section, we present sufficient conditions that guarantee the security of the system model \eqref{eq: actual system} against attacks on the input. We say that the system \eqref{eq: actual system} is \textit{secure with respect to the safety property} for a set $S$ if for all initial conditions $x(0)\in S$,  $x(t)\in S$ for all $t\geq 0$, $u_v\in \mathcal U_v$ and $d$ satisfying Assumption \ref{assum: d bound}. 
% The following lemma provides necessary and sufficient conditions for a system to be not secured with respect to the safety property $P_{safe}$. 
% \begin{Lemma}
% The system is locally vulnerable at point $x_a\in \partial S$ if and only if the following holds:
% \begin{align}\label{eq: attack sufficiency}
%     % \sup_{u_v\in \mathcal U_v}\inf_{u_s\in \mathcal U_s}\{L_fB(x_a) + L_{g_s}B(x_a)u_s +L_{g_v}h_{S}(x_a)u_v\}>\epsilon.
%     \sup_{u_v\in \mathcal U_v}\inf_{u_s\in \mathcal U_s} L_F h_{S}(x_a,u_v,u_s)>0.
% \end{align}
% It is globally vulnerable if the above holds for all $x_a\in \partial S$.  
% \end{Lemma}
% The proof follows immediately from Definition \ref{def: safety secured}. 
% Conversely, 
Given $B$ and $F$, define $H:\mathbb R^n\times\mathbb R^{m_v}\rightarrow\mathbb R$:
\begin{align}\label{eq: H def}
    % H(x,u_v) \coloneqq L_fB(x) + L_{g_s}B(x)u_s(x) +L_{g_v}h_{S}(x)u_v.
    H(x,u_v) \coloneqq \inf_{u_s\in \mathcal U_s}L_F B(x,(u_v,u_s)).
\end{align}
It is not necessary that the zero sublevel set $S$ of the function $B$ is a viability domain for system \eqref{eq: actual system}. Any non-empty sublevel set $S_c \coloneqq \{x\; |\; B(x)\leq -c\}$, where $c\geq 0$, being a viability domain is sufficient for safety of the system. Note that the set $S_c$ is non-empty for $0\leq c\leq -\min\limits_{x\in S}B(x)$. Define $c_M\in \mathbb R$ as
\begin{align}\label{eq: cM}
c_M \coloneqq -\min\limits_{x\in S}B(x),
\end{align}
so that the set of feasible values for $c$ is given as $[0, c_M]$.\footnote{Note that compactness of the set $S$ guarantees existence of $c_M$.} The following result provides sufficient conditions for a system to be secured with respect to the safety property. 
% $P_{safe}$:
\begin{Proposition}\label{lemma: sufficient conditions non-attack}
Suppose there exist $c\in [0, c_M]$ and nonempty $\tilde{\mathcal U}_v\subset\mathcal U_v$ such that
\begin{align}\label{eq: invulnerable cond}
    \sup_{u_v\in \tilde{\mathcal U}_v}H(x,u_v) \leq -l_B\delta \quad \forall x\in \partial S_c,
\end{align}
and the system solutions are uniquely defined in forward time for all $x(0)\in S_c$. Then, for each $d$ satisfying Assumption \ref{assum: d bound}, system \eqref{eq: actual system} is secured with respect to the safety property for the set $S_c$.
% for all $\tau\geq 0$, i.e., $[\mathcal A_\tau]\mathcal S\models P_{safe, S_c}$ for all $\tau\geq 0$.  
% one of the following conditions hold:
% \begin{itemize}
%     \item[1)] $L_{g_v}B(x) = 0$ and $\inf_{u_s\in \mathcal U_s}\{L_fB(x) + L_{g_s}B(x)u_s\}\leq 0$ for all $x\in \partial S$;
%     \item[2)] $\sup_{u_v\in \mathcal U_v}\inf_{u_s\in \mathcal U_s}\{L_fB(x) + L_{g_s}B(x)u_s +L_{g_v}h_{S}(x)u_v\}\leq 0$ for all $x\in \partial S$; 
% \end{itemize}
\end{Proposition}
\begin{proof}
% Note that Definition \ref{def: safety secured} requires that for a point $x_a$ to be vulnerable, the strict inequality \eqref{eq: attack def} must be satisfied for all points in the neighborhood of the point. Thus, excluding a measure zero set, 
Note that 
\begin{align*}
    \inf_{u_s\in\mathcal U_s\atop u_v\in \tilde{\mathcal U}_v}L_F(x,(u_v, u_s)) = \inf_{u_v\in \tilde{\mathcal U}_v}H(x,u_v)\leq \sup_{u_v\in \tilde{\mathcal U}_v}H(x,u_v).
\end{align*}
Thus, from  \eqref{eq: invulnerable cond}, it follows that \eqref{eq: safety cond} holds. Thus, per Lemma \ref{lemma: nec suff safety}, the set $S_c$ is forward invariant and it holds that the system \eqref{eq: actual system} is secured with respect to the safety property for set $S_c$.  
% and it holds that $[\mathcal A_\tau]\mathcal S\models P_{safe, S_c}$ for all $\tau\geq 0$. 
\end{proof}

{\noindent Note that satisfaction of the conditions in Proposition \ref{lemma: sufficient conditions non-attack} implies that for all $x\in \partial S_c$ and $u_v\in \bar{ \mathcal U}_v$,  there exists an input $u_s\in \mathcal U_s$ such that the inequality $L_FB(x,(u_v, u_s))\leq -l_B\delta$ holds. This, in turn, implies that the set $S_c$ is a viability domain for system \eqref{eq: actual system}. Condition \eqref{eq: invulnerable cond} requires checking the inequality $\sup\limits_{u_v\in \tilde{\mathcal U}_v}H(x,u_v)\leq -l_B\delta$ for all points on the boundary of the set $S_c$. Such conditions are commonly used in the literature for control synthesis, assuming that the viability domain is known. However, it is not an easy task to compute a viability domain in practice for a general class of nonlinear systems \textit{a priori}. In the next section, we present a computationally tractable method where we show that checking a modification of the inequality in \eqref{eq: invulnerable cond} on a set of sampling points on the boundary is sufficient. }

% \subsection{Security with respect to convergence property}
% % \textbf{NEEDS MORE WORK, SKIP FOR NOW}

% As shown in \cite{garg2019prescribedTAC}, the domain $D$ in Lemma \ref{lemma: FxTS new}, also called the fixed-time domain of attraction for the set $G$, depends on the ratio $r\coloneqq \frac{\delta_1}{2\alpha}$. In particular, 
% \begin{align}
%      D & = \begin{cases}
%      \mathbb R^n; &  r<1,\\
%     \left\{x\; |\; V(x)\leq k^\mu\left(r-\sqrt{r^2-1}
%     % \frac{\delta -\sqrt{\delta ^2-4\alpha^2}}{2\alpha}
%     \right)^\mu\right\}; & r\geq 1,
%     %  \left\{x\; |\; V(x)\leq k^\mu\Big(\frac{\alpha }{\alpha }\Big)^\frac{\mu}{2}\right\}; & \delta  = 2\alpha,\\
%     \end{cases},
% \end{align}
% where $0<k<1$. We can represent the domain $D$ more compactly as $D = \{x\; |\; V(x)\leq \eta\}$ where $\eta>0$ is a function of $\delta_1$. Using this, define the function $H_G:\mathbb R^n\times\mathbb R^{m_v}\rightarrow\mathbb R$ as
% \begin{align}
%     % H_G(x,u_v) = L_fV(x) + L_{g_s}V(x)u_s(x) +L_{g_v}h_{G}(x)u_v 
%     H_G(x,u_v) = & \inf_{u_s\in \mathcal U_s}L_F V(x,u_v,u_s)-\delta_1V(x) \nonumber\\ & -\alpha V(x)^{\gamma_1}-\alpha V(x)^{\gamma_2},
% \end{align}  
% where $\alpha = \frac{\mu\pi}{2T_{ud}}$, $\gamma_1 = 1+\frac{1}{\mu}$ and $\gamma_2 = 1-\frac{1}{\mu}$ with $\mu>1$. 
% % \textbf{DEFINE alpha1 alpha2 as a function of Tud, clarify the role of Tud}

% The following lemma presents sufficient conditions for the system to be secured with respect to the convergence property:
% \begin{Lemma}\label{lemma: sufficient conditions non-attack for conv}
% If the system solutions are uniquely defined in forward time and there exists $0\leq c\leq \eta$, such that the following holds: 
% \begin{align}\label{eq: invulnerable cond conv}
%     \sup_{u_v\in \mathcal U_v}H_G(x,u_v) \leq 0, \quad \forall x\in D_c,
% \end{align}
% where $D_{c} = \{x\; |\; V(x)\leq \eta-c\}$, then, the system \eqref{eq: actual system} with $d\equiv 0$ is secured with respect to the convergence property for all $\tau\geq 0$, i.e., $[\mathcal A_\tau]\mathcal S\models P_{conv,D_c}$ for all $\tau\geq 0$.  
% \end{Lemma}

% \begin{proof}
% First, note that satisfaction of \eqref{eq: invulnerable cond conv} 
% % implies that $\sup_{u_v\in \mathcal U_v}\inf_{u_s\in \mathcal U_s}L_F V(x,u_v,u_s)\leq 0$ for all $x\in \partial D_c$, and thus, the set $D_c$ is forward-invariant for \eqref{eq: model}. Furthermore, it also 
% implies the
% satisfaction of the conditions of Lemma \ref{lemma: FxTS new}, and thus, it follows that the system trajectories of \eqref{eq: actual system} with $d\equiv 0$ reach the set $V(x)\leq 0$, i.e., the set $K$, within the user-defined time $T_{ud}$.
% \end{proof}

% % For this case, a set $D_c\subset \mathbb R^n$, defined as $D_c \coloneqq \{x\; |\; \sup_{u_v\in \mathcal U_v}H_G(x,u_v)\leq 0 \}\cap \{x\; |\; V(x)\leq \eta-c\}$ for some $\eta>0$, needs to be computed, and rendered forward-invariant, so that the system trajectories do not leave this set under an attack, and per Lemma \ref{lemma: sufficient conditions non-attack for conv}, reach the goal set $K$ within the user-defined time $T_{ud}$. 
% Thus, it is sufficient to find a parameter $0<c<\eta$ such that \eqref{eq: invulnerable cond conv} holds for all $x\in D_c = \{x\; |\; V(x)\leq \eta-c\}$. 

% Note that it is computationally intractable to verify the condition \eqref{eq: invulnerable cond conv}, guaranteeing convergence, in a set $D_c$ for any value of $0<c<\eta$. However, the condition \eqref{eq: invulnerable cond}, guaranteeing forward invariance of a set, only needs to be checked on the boundary of the set. Thus, we resort to a similar method as 

\section{Viability domain under bounded inputs}\label{sec: num method}
In this section, we present numerical algorithms to assess whether given system \eqref{eq: actual system} and the function $B$, there exist $c$ and an input constraint set $\tilde{\mathcal U}_v$ such that condition \eqref{eq: invulnerable cond} holds. First, we present a sampling-based method for evaluating whether the condition \eqref{eq: invulnerable cond} holds by checking a modified inequality at a finite set of sampling points. Then, we propose an iterative method to compute $c$ and the set $\tilde{\mathcal U}_v$.
% to facilitate the sampling-based method.}

% \begin{figure}[t]
% 	\centering
% 	\includegraphics[width=1\columnwidth,clip]{fig_sample_safety.png}
% 	\caption{safe system trajectories under an attack on the inputs. The solid line shows the system trajectories before the attack and the dashed line, after the attack starts at $t = \tau$. The system trajectories without any attack after $t = \tau$ is shown in lighter solid line. }
% 	\label{fig:non-attack safety}
% \end{figure}
\subsection{Viability domain using sampling data}
% If we assume sufficient regularity on the functions $B$ and $F$, numerical methods can be devised to check a modified condition at sampling points while still guaranteeing that the required condition \eqref{eq: invulnerable cond} holds for all $x$ on the boundary of a sublevel set of the function $B$. 
We start by making the following assumption on the regularity of the function $H$ defined in \eqref{eq: H def}.
\begin{Assumption}\label{assum: LC F del B}
The function $\sup_{u_v\in \tilde{\mathcal U}_v}H(\cdot,u_v)$
% $\phi:\mathbb R^n\rightarrow\mathbb R$ defined as
% \begin{align}
%     \phi(x) = \sup_{u_v\in \tilde{\mathcal U}_v}H(x,u_v),
% \end{align}
is Lipschitz continuous on $S$ with constant $l_H>0$. 
\end{Assumption}

\noindent 
% Assumption \ref{assum: LC F del B} implies that the function
% $H$ is Lipschitz continuous in $x$ with constant $l_H = l_Fl_{\partial B}$. 
% \subsubsection{Reduction of safe set}
% Keeping in mind Proposition \ref{lemma: sufficient conditions non-attack}, one can device iterative, numerical approaches to compute a $c$ such that such that \eqref{eq: invulnerable cond} holds for the sublevel set $S_c$. 
% First consider the 2-D case, i.e., the case when $x\in \mathbb R^2$. In this case, the boundary of the set  $S_c$ is a curve, for any $c\in [0, \ c_M]$ (see Figure \ref{fig:2d sampling}). Let $\{x_i\}_{\mathcal I}$ denote the set of $N_p$ sampling data points on the boundary of the sublevel set $S_c$ for a given feasible $c$, with $\mathcal I \coloneqq \{1, 2, \dots, N_p\}$. Let the maximum distance along the curve $S_c$ between the consecutive sampling points be denoted as $d$, i.e., for every $j\in \mathcal I$, the following holds:
% \begin{align}\label{eq: xj xk dist cond}
%   d_{S_c}(x_j, x_{(j+1)\text{mod} N_p})\leq d,
% \end{align}
% where $d_{S_c}(x,y)$ denote the distance between the points $x,y\in S_c$ along the surface $\partial S_c$ and $a~\text{mod}~b$ denotes the remainder when $a$ is divided by $b$. It is easy to verify that $|x_j-x_k|\leq d_{S_c}(x_j,x_k)$ for all $j, k\in \mathcal I$. Also, it is essential that the sampling points \textit{cover} the whole boundary $\partial S_c$. Let $l$ denote the length of the curve $\partial S_c$ and so, the number of sampling points $N_p$ must satisfy:
% \begin{align}\label{eq: sampling points N}
%     N_p \geq \frac{l}{d_m},
% \end{align}
% where $d_m = \min\limits_{j\in \mathcal I}d_{S_c}(x_j, x_{(j+1)\text{mod}N_p})$ denotes the minimum distance between the consecutive sampling points. 
% % \textbf{INTRODUCE THE NOTION OF COMPLETENESS SO THAT THE SET IS COVERED. USE MINIMUM DISTANCE.}
% \begin{figure}[t]
% 	\centering
% 	\includegraphics[width=0.6\columnwidth,clip]{2_D_sampling.png}
% 	\caption{2-D case: Sampling of the curve $\partial S_c$.}
% 	\label{fig:2d sampling}
% \end{figure}
% \begin{Lemma}\label{lemma: sufficient cond 2D}
% Under Assumption \ref{assum: LC F del B}, given the sampling points $\{x_i\}_{\mathcal I}$ satisfying \eqref{eq: xj xk dist cond} and \eqref{eq: sampling points N}, if there exist $0\leq c\leq c_M$ and nonempty $\tilde{\mathcal U}_v\subset\mathcal U_v$ such that 
% \begin{align}\label{eq: sup H cond}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(x_i,u_v)\leq -\frac{l_Hd_a}{2}-l_B\delta \quad \forall i\in \mathcal I,
% \end{align}
% then \eqref{eq: invulnerable cond} holds. 
% % the system \eqref{eq: actual system} with $d\equiv 0$ is secured with respect to the safety property $P_{safe,S_c}$. 
% % \eqref{eq: invulnerable cond}
% % condition 2) of Proposition \ref{lemma: sufficient conditions non-attack}
% % holds for $\tilde h(x) = B(x) + c$. 
% \end{Lemma}
% \begin{proof}
% First, note that the function $H(\cdot,u_v)$ being Lipschitz continuous in $x$ with constant $l_H = l_Fl_{\delta B}$ implies that $\sup_{u_v}H(\cdot,u_v)$ is also Lipschitz continuous in $x$ with the same constant. Now, let $x_j$ and $x_k$ be any two consecutive points in the set $S_c$ satisfying \eqref{eq: xj xk dist cond} such that $j,k\in \mathcal I$. Consider any point $\bar x\in \partial S_c$ on the curve joining $x_j$ and $x_k$. Using Lipschitz continuity of $\sup_{u_v}H(\cdot, u_v)$, it holds that
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq & \sup_{u_v\in \mathcal U_v}H(x_j,u_v) + l_H|\bar x-x_j|\\
%     \leq & -\frac{l_Hd_a}{2}-l_B\delta + l_Hd{S_c}(\bar x, x_j),
% \end{align*}
% where the last inequality follows from \eqref{eq: sup H cond}. Similarly, we can obtain the following inequality:
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq & -\frac{l_Hd_a}{2}-l_B\delta + l_Hd{S_c}(\bar x, x_k).
% \end{align*}
% Thus, we obtain that \small{
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}\hspace{-5pt}H(\bar x,u_v) & \leq -\frac{l_Hd_a}{2}-l_B\delta + \frac{l_H}{2}(d_{S_c}(\bar x, x_j)+d_{S_c}(\bar x, x_k)).
% \end{align*}}\normalsize
% Note that $d_{S_c}(\bar x, x_j)+d_{S_c}(\bar x, x_k) = d_{S_c}(x_j, x_k)$. Using this and \eqref{eq: xj xk dist cond}, we obtain\small{
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}\hspace{-5pt}H(\bar x,u_v) & \leq -\frac{l_Hd_a}{2}-l_B\delta + \frac{l_H}{2}d_{S_c}(x_j, x_k) \leq-l_B\delta,
% \end{align*}}\normalsize
% which implies that $H(\bar x,u_v)\leq -l_B\delta$ for all $\bar x\in \partial S$ on the curve between the points $x_j$ and $x_k$. Under \eqref{eq: sampling points N}, the sampling points cover the whole curve $\partial S_c$, the same argument can be used for all consecutive points $x_j, x_k$ in $\{x_i\}_{\mathcal I}$ and it can be concluded that $\sup_{u_v\in \mathcal U_v}H(\bar x,u_v)\leq -l_B\delta$ for all $\bar x\in \partial S$. 
% % Thus, per Proposition \ref{lemma: sufficient conditions non-attack}, the system is secured with respect to the safety property.
% \end{proof}
% % In plain words, if the distance between the consecutive sampling-points ${x_i}$ is no more than $\frac{2\gamma}{l_H}$, then satisfaction of \eqref{eq: sup H cond} implies that the system is secured with respect to the set $S_c = \{x\; |\; B(x)\leq -c\}$.

% \subsubsection{Case when $S\subset \mathbb R^3$}
First, to illustrate the method, we consider the 3-D case, i.e., when $x\in \mathbb R^3$. 
% \textit{Triangulation} of surface in $\mathbb R^3$ is defined by the authors in \cite{hartsfield1991clean} as follows.
% \begin{Definition}\label{def: triangulation}
%   A polyhedron $P$ with its vertices on a closed surface $S\subset \mathbb R^3$ is called a \textnormal{triangulation} of $S$, or said to \textnormal{triangulate} the surface $S$, if each face of $P$ is a triangle with three distinct vertices, and the intersection of any two distinct triangles is either empty, a single vertex, or a single edge. 
% \end{Definition}
If the compact set $S\subset \mathbb R^3$ is diffeomorphic to a unit sphere in $\mathbb R^3$, then the sampling points on the boundary of the unit sphere can be used to obtain the points on the boundary of $S_c$. Thus, without loss of generality, we can study the case when $S\subset \mathbb R^3$ is a unit sphere with center $x_o\in \mathbb R^3$. Let $\{x_i\}_{\mathcal I}$, with each $x_i\in \partial S_c$, denote the set of $N_p$ sampling data points on the boundary of the sublevel set $S_c$ for a given $c\in [0, c_M]$ with $c_M$ defined in \eqref{eq: cM} and $\mathcal I \coloneqq \{1, 2, \dots, N_p\}$. The sampling points $\{x_i\}_{\mathcal I}$ are such that they constitute a polyhedron $P_{\mathcal I}$ with $N_f>0$ triangular faces, $T_1, T_2, \dots, T_{N_f}$, such that $P_{\mathcal I}$ \textit{triangulates} the boundary $\partial S_c$, i.e., the intersection of any two distinct triangles is either empty, a single vertex, or a single edge. Figure \ref{fig:3d sampling} shows an example of triangulation of a unit sphere in $\mathbb R^3$. Interested readers on algorithms and details on triangulation are referred to \cite{oudot2003provably}, and the references therein.

Note that a tetrahedron is the \textit{minimal} triangulation (i.e., a triangulation with minimum number of triangular faces) for a unit sphere. Using geometric arguments, it is easy to show that the minimum possible value of the maximum of the inter-vertex distances for a tetrahedron inscribed in a unit sphere is $\sqrt{3}$. The corresponding arc-length along the boundary of the unit sphere (denote as $d_a$) is $2\sin^{-1}\sqrt{\frac{3}{4}}$. It follows that if $d_a\leq 2\sin^{-1}\sqrt{\frac{3}{4}}$, then there must be at least $N_p = 4$ points in the polyhedron. Finally, with $0\leq r_c\leq 1$ being the radius of the sphere $S_c$,\footnote{If the set $S_c$ is defined as $S_c = \{x\; |\; |x|^2-1\leq -c\}$, then $r_c = \sqrt{1-c}$.} the corresponding arc-length for $S_c$ is
\begin{align}\label{eq: def dM}
    d_M \coloneqq 2r_c\sin^{-1}\sqrt{\frac{3}{4}}.
\end{align}

%%% Old version Lemma 3

% To ensure that there are enough sampling points for the boundary, we make the following assumption. 

% \begin{Assumption}\label{assum: max dist tring}
% Given $c\in [0,  c_M]$ and $d_a\in \begin{bmatrix}0, d_M\end{bmatrix}$, the sampling points $\{x_i\}_{\mathcal I}$ are such that for each $x\in \partial S_c$, there exists a triangular face $T_j$ with vertices $x_{j_1}, x_{j_2}, x_{j_3}\in \{x_i\}_{\mathcal I}$, where $j\in \{1, 2, \dots, N_f\}$, of the polyhedron $P_{\mathcal I}$ generated by $\{x_i\}_{\mathcal I}$, such that $x_o+\theta (x-x_o)\in T_j$ for some $0\leq \theta\leq 1$, and the following holds:
% \begin{align}\label{eq: xj xk dist cond 3d}
%   \max_{l\neq m \atop l, m = 1, 2, 3}d_{S_c}(x_{j_l}, x_{j_m})\leq d_a,
% \end{align}
% where $d_{S_c}(x,y)$ denotes the shortest  arc-length between the points
% % smallest length of the curves within the boundary $\partial S_c$ connecting the points 
% $x,y\in \partial S_c$.
% \end{Assumption}

% % \begin{Assumption}\label{assum: max dist tring}
% % Given $c\in [0,  c_M]$, $d\in \begin{bmatrix}0,  2\sin^{-1}\sqrt{\frac{3}{4r_c}}\end{bmatrix}$, and the sampling points $\{x_i\}_{\mathcal I}$, for each $x\in \partial S_c$, there exists  $x_{j_1}, x_{j_2}, x_{j_3}\in \{x_i\}_{\mathcal I}$ such that $x_o+\theta (x-x_o)\in T_j$ for some $0\leq \theta\leq 1$, where $T_j$ is the convex hull of the points $x_{j_1}, x_{j_2}, x_{j_3}$, and the following holds:
% % \begin{align}\label{eq: xj xk dist cond 3d}
% %   \max_{l\neq m \atop l, m = 1, 2, 3}d_{S_c}(x_{j_l}, x_{j_m})\leq d,
% % \end{align}
% % where $d_{S_c}(x,y)$ denotes the the  shortest  arc-length  between the points
% % % smallest length of the curves within the boundary $\partial S_c$ connecting the points 
% % $x,y\in S_c$. 
% % \end{Assumption}
% In plain words, Assumption \ref{assum: max dist tring} requires that for each point $x\in \partial S_c$, the line joining the center $x_o$ and $x$ intersects a triangular face of the polyhedron such that the distance along the boundary $\partial S_c$ between the vertices of this face is bounded by $d_a$. Note that smaller $d_a$ requires larger number of sampling points $N_p$ for satisfaction of Assumption \ref{assum: max dist tring}. 
% % Finally, it is easy to verify that $|x-y|\leq d_{S_c}(x_j,x_k)$ for all $j, k\in \mathcal I$, i.e., the Euclidean distance between two sampling points is less or equal than their distance computed along the boundary $\partial S_c$. 
% % We can now state the following result. 
% % We assume that we have enough sampling points that are sufficient to cover the surface $\partial S_c$. 
% %, i.e., the distance between the consecutive sampling points along the surface $\partial S_c$ is no greater than $\frac{\gamma}{l_H}$. 

% \begin{figure}[t]
% 	\centering
% 	\includegraphics[width=0.4\columnwidth,clip]{3_D_sampling.png}
% 	\caption{3-D case: Triangulating sampling of the boundary $\partial S_c$.}
% 	\label{fig:3d sampling}
% \end{figure}

% \begin{Lemma}\label{lemma: sufficient cond 3D}
% Suppose that the function $H$ defined in \eqref{eq: H def} satisfies Assumption \ref{assum: LC F del B}. Given $c\in [0, c_M]$, $d_a\in \begin{bmatrix}0,  d_M\end{bmatrix}$, and the sampling points $\{x_i\}_{\mathcal I}$
% % such that the resulting polyhedron $P_{\mathcal I}$ triangulates the boundary $\partial S_c$, 
% satisfying Assumption \ref{assum: max dist tring}, if the following holds
% \begin{align}\label{eq: sup H cond 3D}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(x_i,u_v)\leq -l_Hd_a-l_B\delta \quad \forall i\in \mathcal I,
% \end{align}
% where $l_B$ is the Lipschitz constant for $B$ and $\delta, l_H$ are as defined in Assumptions \ref{assum: d bound} and \ref{assum: LC F del B}, respectively,
% then, \eqref{eq: invulnerable cond} holds.
% % the system is secured with respect to the safety property $P_{safe,S_c}$.  
% % then, \eqref{eq: invulnerable cond}
% % condition 2) of Proposition \ref{lemma: sufficient conditions non-attack}
% % holds for $\tilde h(x) = B(x) + c$. 
% \end{Lemma}
% \begin{proof}
% % Suppose there exists $c\in [0, c_M]$ such that \eqref{eq: sup H cond 3D} holds, and a corresponding $d\in \begin{bmatrix}0,  2\sin^{-1}\sqrt{\frac{3}{4r_c}}\end{bmatrix}$ such that Assumption \ref{assum: max dist tring} holds.
% With $c\in [0, c_M]$, the set $S_c$ is non-empty, and with $d_a\in \begin{bmatrix}0,  d_M\end{bmatrix}$, there exist sufficient points $N_p$ to have a polyhedron that can triangulate the boundary $\partial S_c$. Now, consider any point $\bar x\in \partial S_c$. Under Assumption \ref{assum: max dist tring}, for every $\bar x\in \partial S_c$, there exists a triangular face $T_j$ with coordinates $x_{j_1}, x_{j_2}, x_{j_3}\in \{x_i\}_{\mathcal I}$   satisfying \eqref{eq: xj xk dist cond 3d} and $0\leq \theta\leq 1$ such that $x_o+\theta(\bar x-x_o)\in T_j$ . Using Lipschitz continuity of $\sup_{u_v}H(\cdot, u_v)$ per Assumption \ref{assum: LC F del B}, the following holds for all $x, \bar x\in \partial S_c$:
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq & \sup_{u_v\in \tilde{\mathcal U}_v}H(x,u_v) + l_H|\bar x-x|.
% \end{align*}
% For $x = x_i$, $i\in \mathcal I$, using \eqref{eq: sup H cond 3D} and the fact that $|x-y|\leq d_{S_c}(x,y)$ for all $x, y\in \partial S_c$, we obtain that
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v)\leq & -l_Hd_a-l_B\delta + l_Hd_{S_c}(\bar x, x_i), \; \forall i\in \mathcal I.
% \end{align*}
% % where the last inequality follows from \eqref{eq: sup H cond 3D} and 
% Using the above inequality for $x_i = x_{j_1}, x_{j_2}$ and $x_{j_3}$, we obtain that for all $\bar x\in \partial S_c$, {\small
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq & -l_Hd_a -l_B\delta+ \frac{l_H}{3}\sum_{k = 1}^3d_{S_c}(\bar x, x_{j_k}).
% \end{align*}}\normalsize
% Since $\bar x$ lies in the triangular face $T_j$, it holds that $d_{S_c}(\bar x, x_{j_k})\leq d_{S_c}(x_{j_l}, x_{j_k})$ for $l\neq k$, $l, k \in \{1, 2, 3\}$. Using this, we obtain{\small
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq & -l_Hd_a -l_B\delta+ \frac{l_H}{3}\left(3\max_{l \neq m, \atop l, m = 1, 2, 3}d_{S_c}(x_{j_l}, x_{j_m})\right).
% \end{align*}}\normalsize
% Moreover, using \eqref{eq: xj xk dist cond 3d}, it follows that
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq -l_Hd_a -l_B\delta+l_Hd_a = -l_B\delta,
% \end{align*}
% for all $\bar x\in \partial S_c$, which completes the proof. 
% % in the projection of the triangle $T_j$ on $\partial S_c$. Under Assumption \ref{assum: max dist tring}, using the similar arguments for sampling points on all of the triangular faces on the boundary, it can be concluded that $\sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v)\leq -l_B\delta$ for all $\bar x\in \partial S$.
% \end{proof}

% Lemma \ref{lemma: sufficient cond 3D} provides a computationally tractable method of assessing whether \eqref{eq: invulnerable cond} can be satisfied for a given value of $c$ and the constraint set $\tilde{\mathcal U}_v$ by checking the inequality \eqref{eq: sup H cond 3D} at a finite number of points. Note that for a given $F, B, \tilde{\mathcal U}_v$ and $\delta$, a smaller value of $d_a$ implies that the right-hand side of \eqref{eq: sup H cond 3D} is less negative, thus, making it easier to satisfy the inequality. At the same time, due to \eqref{eq: def dM}, a smaller value of $d_a$ requires more sampling points $N_p$, and hence, checking the inequality at more points. Thus, there is a trade-off between the ease of satisfaction of \eqref{eq: sup H cond 3D} and the number of points at which the inequality should be checked.

%%% Old version Lemma 3 end


% To ensure that there are enough sampling points for the boundary, we make the following assumption. 

% \begin{Assumption}\label{assum: max dist tring}
\noindent Now, to ensure that they are enough sampling points, the following conditions can be imposed on $\{x_i\}_{\mathcal I}$ for a given $c\in [0,  c_M]$ and $d_a\in \begin{bmatrix}0, d_M\end{bmatrix}$ 
\begin{itemize}
    \item For each $x\in \partial S_c$, there exists a triangular face $T_j$ with vertices $x_{j_1}, x_{j_2}, x_{j_3}\in \{x_i\}_{\mathcal I}$, of the polyhedron $P_{\mathcal I}$ generated by $\{x_i\}_{\mathcal I}$, such that $x_o+\theta (x-x_o)\in T_j$ for some $0\leq \theta\leq 1$; and 
    \item The following holds:
\begin{align}\label{eq: xj xk dist cond 3d}
  \max_{l\neq m \atop l, m = 1, 2, 3}d_{S_c}(x_{j_l}, x_{j_m})\leq d_a,
\end{align}
where $d_{S_c}(x,y)$ denotes the shortest  arc-length between the points $x,y\in \partial S_c$.
\end{itemize}

In plain words, the above conditions require for each point $x\in \partial S_c$, the line joining the center $x_o$ and $x$ intersects a triangular face of the polyhedron such that the distance along the boundary $\partial S_c$ between the vertices of this face is bounded by $d_a$. Note that smaller $d_a$ requires larger number of sampling points $N_p$. 
% for satisfaction of Assumption \ref{assum: max dist tring}. 
% Finally, it is easy to verify that $|x-y|\leq d_{S_c}(x_j,x_k)$ for all $j, k\in \mathcal I$, i.e., the Euclidean distance between two sampling points is less or equal than their distance computed along the boundary $\partial S_c$. 
% We can now state the following result. 
% We assume that we have enough sampling points that are sufficient to cover the surface $\partial S_c$. 
%, i.e., the distance between the consecutive sampling points along the surface $\partial S_c$ is no greater than $\frac{\gamma}{l_H}$. 
\begin{figure}[t]
	\centering
	\includegraphics[width=0.3\columnwidth,clip]{3_D_sampling.png}
	\caption{3-D case: Triangulating sampling of the boundary $\partial S_c$.}
	\label{fig:3d sampling}
\end{figure}
% \begin{Lemma}\label{lemma: sufficient cond 3D}
Now, we show that 
% the function $H$ defined in \eqref{eq: H def} satisfies Assumption \ref{assum: LC F del B}. Given $c\in [0, c_M]$, $d_a\in \begin{bmatrix}0,  d_M\end{bmatrix}$, and the sampling points $\{x_i\}_{\mathcal I}$
% such that the resulting polyhedron $P_{\mathcal I}$ triangulates the boundary $\partial S_c$, 
% satisfying Assumption \ref{assum: max dist tring}, if 
if the following holds
\begin{align}\label{eq: sup H cond 3D}
    \sup_{u_v\in \tilde{\mathcal U}_v}H(x_i,u_v)\leq -l_Hd_a-l_B\delta \quad \forall i\in \mathcal I,
\end{align}
where $l_B$ is the Lipschitz constant for $B$ and $\delta, l_H$ are as defined in Assumptions \ref{assum: d bound} and \ref{assum: LC F del B}, respectively,
then, \eqref{eq: invulnerable cond} holds.
% the system is secured with respect to the safety property $P_{safe,S_c}$.  
% then, \eqref{eq: invulnerable cond}
% condition 2) of Proposition \ref{lemma: sufficient conditions non-attack}
% holds for $\tilde h(x) = B(x) + c$. 
% \end{Lemma}
% \begin{proof}
% Suppose there exists $c\in [0, c_M]$ such that \eqref{eq: sup H cond 3D} holds, and a corresponding $d\in \begin{bmatrix}0,  2\sin^{-1}\sqrt{\frac{3}{4r_c}}\end{bmatrix}$ such that Assumption \ref{assum: max dist tring} holds.
With $c\in [0, c_M]$, the set $S_c$ is non-empty, and with $d_a\in \begin{bmatrix}0,  d_M\end{bmatrix}$, there exist sufficient points $N_p$ to have a polyhedron that can triangulate the boundary $\partial S_c$. Under the conditions imposed on $\{x_i\}_{\mathcal I}$, for every $\bar x\in \partial S_c$, there exists a triangular face $T_j$ with coordinates $x_{j_1}, x_{j_2}, x_{j_3}\in \{x_i\}_{\mathcal I}$   satisfying \eqref{eq: xj xk dist cond 3d} and $0\leq \theta\leq 1$ such that $x_o+\theta(\bar x-x_o)\in T_j$. Using Lipschitz continuity of $\sup_{u_v}H(\cdot, u_v)$ per Assumption \ref{assum: LC F del B}, it holds that $\sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq  \sup_{u_v\in \tilde{\mathcal U}_v}H(x,u_v) + l_H|\bar x-x|$,
% the following holds 
for all $x, \bar x\in \partial S_c$.
% \begin{align*}
% \end{align*}
For $x = x_i$, $i\in \mathcal I$, using \eqref{eq: sup H cond 3D} and the fact that $|x-y|\leq d_{S_c}(x,y)$ for all $x, y\in \partial S_c$, we obtain that
\begin{align*}
    \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v)\leq & -l_Hd_a-l_B\delta + l_Hd_{S_c}(\bar x, x_i), \; \forall i\in \mathcal I.
\end{align*}
% where the last inequality follows from \eqref{eq: sup H cond 3D} and 
% Using the above inequality for $x_i = x_{j_1}, x_{j_2}$ and $x_{j_3}$, we obtain that for all $\bar x\in \partial S_c$, 
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq & -l_Hd_a -l_B\delta+ \frac{l_H}{3}\sum_{k = 1}^3d_{S_c}(\bar x, x_{j_k}).
% \end{align*}
Since the projection of $\bar x$ lies in the triangular face $T_j$, it holds that $d_{S_c}(\bar x, x_{j_k})\leq d_{S_c}(x_{j_l}, x_{j_k})$ for $l\neq k$, $l, k \in \{1, 2, 3\}$. Using this and \eqref{eq: xj xk dist cond 3d}, we obtain
% {\small
% \begin{align*}
%     \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq & -l_Hd_a -l_B\delta+ \frac{l_H}{3}\left(3\max_{l \neq m, \atop l, m = 1, 2, 3}d_{S_c}(x_{j_l}, x_{j_m})\right).
% \end{align*}}\normalsize
% Moreover, using \eqref{eq: xj xk dist cond 3d}, it follows that
\begin{align*}
    \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq -l_Hd_a -l_B\delta+l_Hd_a = -l_B\delta, \; \forall \bar x\in \partial S_c.
\end{align*}
% for all $\bar x\in \partial S_c$.
% in the projection of the triangle $T_j$ on $\partial S_c$. Under Assumption \ref{assum: max dist tring}, using the similar arguments for sampling points on all of the triangular faces on the boundary, it can be concluded that $\sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v)\leq -l_B\delta$ for all $\bar x\in \partial S$.
% \end{proof}
Thus, checking the inequality \eqref{eq: sup H cond 3D} at a finite number of points is a computationally tractable method for assessing whether \eqref{eq: invulnerable cond} holds for a given $c$ and $\tilde{\mathcal U}_v$. Note that for a given $F, B, \tilde{\mathcal U}_v$ and $\delta$, a smaller value of $d_a$ implies that the right-hand side of \eqref{eq: sup H cond 3D} is less negative, thus, making it easier to satisfy the inequality. At the same time, due to \eqref{eq: xj xk dist cond 3d}, a smaller value of $d_a$ requires more sampling points $N_p$, and hence, checking the inequality at more points. Thus, there is a trade-off between the ease of satisfaction of \eqref{eq: sup H cond 3D} and the number of points at which the inequality should be checked.

% \begin{Remark}
% While we present the specific cases of 2D and 3D for the ease of visualization, the presented method can be readily extended to $n-$dimension, i.e., the case when $S_c\in \mathbb R^n$, using a sampling for the corresponding $(n-1)$ dimensional manifold $\partial S_c$. In particular, using the notion of maximum distance $d$ between the consecutive points, noting that a convex combination of affinely independent $n$ points can cover a portion of the surface $\partial S_c$ with non-zero Legesgue measure and sampling the surface $\partial S_c$ using a $(n-1)-$simplex (see e.g., \cite{karimipour2010simplex}), Lemma \ref{lemma: sufficient cond 3D} can be used for a general $n-$dimensional system.
% \end{Remark}
% In plain words, if the distance between the consecutive sampling-points ${x_i}$ is no more than $\frac{\gamma}{l_H}$, then satisfaction of \eqref{eq: sup H cond} implies that the system is secured with respect to the set $S_c = \{x\; |\; B(x)\leq -c\}$.
% \subsubsection{General case of $S\subset \mathbb R^n$} 
The above arguments can be generalized to the $n-$dimensional case. Using the sampling approach in \cite{leopardi2009diameter} for a unit sphere in $n-$dimension, combined with Delaunay Triangulation of the sampling points (see e.g., \cite{de1997computational}), an $(n-1)-$dimensional \textit{simplex} can be obtained. If the compact set $S\subset \mathbb R^n$ is diffeomorphic to a unit $(n-1)-$sphere, then sampling points on the boundary of $S$ can be obtained using the sampling points for the $(n-1)-$unit sphere. Thus, we study the case when the set $S$ is an $(n-1)-$unit sphere.
% make the following assumption.
% \begin{Assumption}\label{assum: diffe sphere}
% \end{Assumption}
% Under the above assumption, the diffeomorphism can be used to obtain  

Let $\{x_i\}_{\mathcal I}$, with each $x_i\in \partial S_c$, denote the set of $N_p$ sampling data points on the boundary of the sublevel set $S_c$ for a given $c\in [0, c_M]$ with $c_M$ defined in \eqref{eq: cM} and $\mathcal I \coloneqq \{1, 2, \dots, N_p\}$. The sampling poins $\{x_i\}_{\mathcal I}$ constitute a simplex $\mathcal S_{\mathcal I}$ with $N_f>0$ faces, $\mathcal X_1, \mathcal X_2, \dots, \mathcal X_{N_f}$. 
% The convex-hull of a $(n-1)$-simplex covers a subset of $n-$dimensional object with non-zero Lebesgue measure. Thus, using the similar ideas employed for triangulating a surface in 3D, one case uses $(n-1)-$simplex to sample a boundary of $n$-dimensional set $S$.  
For a unit sphere in $\mathbb R^n$, the minimum number of points in the simplex is $(n+1)$, and the minimum possible value of the maximum of the lengths of its edges is $\sqrt{\frac{2(n+1)}{n}}$. The length, denoted as $d_a$, of the corresponding arc-length on the boundary $\partial S_c$ is $2r_c\sin^{-1}\sqrt{\frac{(n+1)}{2n}}$, where $0\leq r_c\leq 1$ is the radius of the sphere $S_c$. Thus, with $d_a\leq 2r_c\sin^{-1}\sqrt{\frac{(n+1)}{2n}}$, there must be at least $(n+1)$ points in the simplex. For the sake of brevity, define $d_{M,n}\coloneqq 2r_c\sin^{-1}\sqrt{\frac{(n+1)}{2n}}$. We make the following assumption on the sampling points $\{x_i\}_{\mathcal I}$.  
\begin{Assumption}\label{assum: max dist tring nD}
Given $c\in [0,  c_M]$, the sampling points $\{x_i\}_{\mathcal I}$ and $d_a\in \begin{bmatrix}0,  d_M\end{bmatrix}$, for each $x\in \partial S_c$, there exists a face $\mathcal X_j$ with vertices $\{x_{j_1}, x_{j_2}, \dots, x_{j_n}\}\in \{x_i\}_{\mathcal I}$, where $j\in \{1, 2, \dots, N_f\}$, of the simplex $\mathcal S_{\mathcal I}$ generated by $\{x_i\}_{\mathcal I}$, such that $x_o+\theta (x-x_o)\in \mathcal X_j$ for some $0\leq \theta\leq 1$, and the following holds:
\begin{align}\label{eq: xj xk dist cond nd}
   \max_{l\neq m \atop l, m = 1, 2, \dots, n}d_{S_c}(x_{j_l}, x_{j_m})\leq d_a,
\end{align}
where $d_{S_c}(x,y)$ denotes the shortest arc-length between the points $x,y\in \partial S_c$.
\end{Assumption}

% Assuming that the maximum distance between any pair of vertices of this simplex satisfies \eqref{eq: xj xk dist cond 3d}, 
% The following result can now be stated. 
We have the following result when $S$ is $(n-1)-$unit sphere. 

\begin{Theorem}\label{thm: sufficient sup H cond}
% Consider a unit sphere $S\subset \mathbb R^n$.
Suppose that the function $H$ defined in \eqref{eq: H def} satisfies Assumption \ref{assum: LC F del B}. Given $c\in [0, c_M]$, $d_a\in \begin{bmatrix}0,  d_{M,n}\end{bmatrix}$, and the sampling points $\{x_i\}_{\mathcal I}$,
% such that the resulting polyhedron $P_{\mathcal I}$ triangulates the boundary $\partial S_c$,
if Assumption \ref{assum: max dist tring nD} and \eqref{eq: sup H cond 3D} hold, 
% Given $d>0$, the sampling points $\{x_i\}_{\mathcal I}$ on the boundary $\partial S_c$ satisfying Assumption \ref{assum: max dist tring nD}, if there exists $0\leq c\leq c_M$ such that \eqref{eq: sup H cond 3D} 
% and Assumption \ref{assum: max dist tring} holds, 
then, \eqref{eq: invulnerable cond} holds.
\end{Theorem}
\begin{proof}
With $c\in [0, c_M]$, the set $S_c$ is non-empty, and with $d_a\in \begin{bmatrix}0,  d_M\end{bmatrix}$, there exist sufficient points $N_p$ to have a simplex. Now, consider any point $\bar x\in \partial S_c$. Under Assumption \ref{assum: max dist tring nD}, for every $\bar x\in \partial S_c$, there exists a face $\mathcal X_j$ of the simplex $\mathcal S_{\mathcal I}$, such that the line joining the center of the sphere $S_c$ and the point $\bar x$ lies on this face. 
% Consider the $n$ vertices $\{x_{j_1},x_{j_2}, \dots, x_{j_n}\}$ of an arbitrary simplex $\mathcal X_j$ used for sampling the boundary $\partial S_c$ and consider any point $\bar x\in \mathbb R^n$ in the projection of $\mathcal X_j$ on $\partial S_c$. 
Using Lipschitz continuity of $\sup_{u_v}H(\cdot, u_v)$ under Assumption \ref{assum: LC F del B} and \eqref{eq: sup H cond 3D}, it holds that
\begin{align*}
    \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq & \sup_{u_v\in \mathcal U_v}H(x,u_v) + l_H|\bar x-x|\\
    \leq & -l_Hd_a-l_B\delta + l_H|\bar x-x|,
\end{align*}
for all $x, \bar x\in \partial S_c$. 
% Using the above inequality for the $n$ vertices $x_{j_1}, x_{j_2}, \dots, x_{j_n}$, of $\mathcal X_j$, we obtain that
% \begin{align*}
%      \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) \leq & -l_Hd_a-l_B\delta + \frac{1}{n}l_H\sum_{i= 1}^n |\bar x-x_{j_i}|\\
%      \leq &  -l_Hd_a-l_B\delta + \frac{1}{n}l_H( n \max_{i\in \{1, \dots, n\}}|\bar x-x_{j_i}|)
% \end{align*}
% Finally, 
Using the inequality for $x = x_{j_i}$, $i\in \{1, \dots, n\}$ and the fact that $|\bar x-x_{j_i}|\leq d_{S_c}(\bar x,x_{j_i})\leq d_{S_c}(x_{j_k},x_{j_i})$ for any $k\neq i$, $k\in \{1, \dots, n\}$ and \eqref{eq: xj xk dist cond nd}, we obtain that
\begin{align*}
     \sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v)
     \leq & -l_Hd_a-l_B\delta + l_H d_a =  -l_B\delta
\end{align*}
for all $\bar x\in \partial S_c$, which completes the proof.
\end{proof}

Note that there are three set of parameters that can facilitate satisfaction of \eqref{eq: sup H cond 3D} in the following manner:
\begin{itemize}
    \item Set $\tilde{\mathcal U}_v$: smaller $\tilde{\mathcal U}_v$ makes it easier to satisfy \eqref{eq: sup H cond 3D};
    \item Parameter $c$: larger value of $c$ results in smaller values of $d_M$, thus, reducing the right-hand side of \eqref{eq: sup H cond 3D}, and making it easier to satisfy it; and
    \item Number of sampling points $N_p$: larger $N_p$ results in smaller value of $d_{M,n}$.
\end{itemize}

Based on these observations, an iterative algorithm can be formulated to check whether there exists a feasible $c$ and a non-empty set $\tilde{\mathcal U}_v$, such that \eqref{eq: sup H cond 3D} holds. 

\subsection{Iterative algorithm}
% \subsubsection{Computation of $c$}: 
We formulate our algorithm with the following steps:
\begin{itemize}
    \item[1)] For a given value of $0\leq c\leq c_M$, $\tilde{\mathcal U}_v$ and number of sampling points $N_p$, sample $\{x_i\}_{\mathcal I}$ from the set $\partial S_c$ and check if \eqref{eq: sup H cond 3D} holds for all the sampling points;
    \item[2)] Shrink $\tilde{\mathcal U}_v$,  increase $c$ and repeat steps 1)-2) until the condition \eqref{eq: sup H cond 3D} is satisfied for all the sampling points, or there does not exist a $c$ and a non-empty set $\tilde{\mathcal U}_v$;
    \item[3)] Increase $N_p$ and repeat steps 1)-3) until \eqref{eq: sup H cond 3D} holds or the maximum value ($N_{max}$) of $N_p$ is reached.
\end{itemize}
Using these steps, we propose Algorithm \ref{algo: iter U c comb} which returns a feasible $c$ and a set $\tilde{\mathcal U}_v$ such that safety is guaranteed for all $x\in S_c$ and $u_v\in \tilde{\mathcal U}_v$. In other words, this algorithm can compute the set of initial conditions $S_c$, and the set of \textit{tolerable} attacked inputs via $\tilde{\mathcal U}_v$ such that the system can satisfy the safety property under attacks. The order in which the parameters $c, \tilde{\mathcal U}_v$, and $N_p$ are tuned can be changed, which can potentially change the output of the algorithm. 
% In brief, Algorithm \ref{algo: iter U c comb}, for a given $c$, shrinks the set $\mathcal U_v$ until the condition \eqref{eq: sup H cond 3D} is satisfied or the set $\mathcal U_v$ becomes empty. If the set $\mathcal U_v$ becomes empty, it is re-initialized, and the value of $c$ is increased, or equivalently, the set $S_c$ is shrunk, until the condition \eqref{eq: sup H cond 3D} is satisfied. This process is repeated until the set $S_c$ becomes empty, i.e., $c = c_M$. 

\begin{algorithm}[h]\label{algo: iter U c comb}
\SetAlgoLined
\KwData{$f,g_v, g_s,\mathcal U_v, \mathcal U_s, B, d_a, \varepsilon_1, \varepsilon_2, \delta, N_{max}, N_{c0}$}
% \KwResult{Input constraint set $\tilde{\mathcal U}_v$ and $c$}
\textbf{Initialize: }$\tilde{\mathcal U}_v = \mathcal U_v, c = 0, N_p = N_{c0}$\;
\While{$N_p< N_{max}$}
{
 \While{$c\leq c_M$}{
 Sample $\{x_i\}_{\mathcal I}$ from $\{B(x)\leq -c\}$\;
 \While{$\tilde{\mathcal U}_v\neq \emptyset$}{
  \lIf{\footnotesize{$\{i\in \mathcal I\; |\; H(x_i, u_v)\!>\!-l_Hd_a\!+\!l_B\delta\} \neq \emptyset $}\label{line: h s U}}{
  
   $\hspace{10pt}\tilde{\mathcal U}_v = \tilde{\mathcal U}_v\ominus \varepsilon_1 $\ \label{step: Ua reduction}
%   $I = \tilde I$;
   }
}
 \lIf {$\tilde{\mathcal U}_v = \emptyset$}{
 
 $\hspace{10pt}c = c+\varepsilon_2$;\\
 $\hspace{10pt}\tilde{\mathcal U}_v = \mathcal U_v$}
 }
 $N_p = 2\; N_p$; \\
 $c = 0$;
 }
 \textbf{Return: }$\bar {\mathcal U}_v, c$\;
 \caption{Iterative method for computing $\tilde{\mathcal U}_v, c$}
\end{algorithm}

\begin{Remark}\label{rem: attack model 1}
If it is unknown which components of the input are vulnerable, then all possible combinations of $u_v$ and $u_s$ can be considered, and Algorithm \ref{algo: iter U c comb} can be used to compute $c$ for each such combination. Then, the maximum of all such values can be used to define the set $S_c$, guaranteeing the system's security against attack on any control inputs. 
% For example, in the case of four inputs (i.e., $m = 4$), there are a total of fourteen such possible combinations.  
\end{Remark}

\begin{Remark}
The computational complexity of Algorithm \ref{algo: iter U c comb} is only a function of the number of sampling points $N_p$ (which, in principle, is a user-defined parameter) and is independent of the non-linearity of the function $F$, and linear in the dimension $n$. Thus, unlike reachability based tools in \cite{bansal2017hamilton,choi2021robust} where the computational complexity grows exponentially with the system dimension $n$, or SOS based tools \cite{wang2018permissive} that are only applicable to a specific class of systems with linear or polynomial dynamics, Algorithm \ref{algo: iter U c comb} can be used for general nonlinear system with high dimension.  
\end{Remark}
% \subsubsection{Computation of the set $\mathcal U_v$}\label{sec: set Ua design}
% As discussed in \cite{giraldo2020daria},  one can device iterative, numerical approaches to compute a particular set $\mathcal U_v$ such that the conditions of Proposition \ref{lemma: sufficient conditions non-attack} hold for a particular value of $c$, e.g.,  $c = 0$, when the viability set is the largest. The main idea is to reduce the set $\mathcal U_v$ so that the condition \eqref{eq: sup H cond} holds for all the sampling points $\{x_i\}_{I_0}$, i.e., on the boundary of the safe set $S$. The iterative algorithm is given in Algorithm \ref{algo: iter U}. In this case as well, $\gamma = \frac{l_Hd_a}{2}$ for 2D case and $\gamma = l_Hd_a$ for 3D case in Line \ref{line: h s U}. {The algorithm shrinks the set $\mathcal U_v$ until the condition \eqref{eq: sup H cond} for 2D (\eqref{eq: sup H cond 3D} for 3D) is satisfied or the set $\mathcal U_v$ becomes empty. }

% \begin{algorithm}\label{algo: iter U}
% \SetAlgoLined
% \KwData{$f,g_v, g_s,\mathcal U_s, B, \delta, \gamma$}
% \KwResult{Input constraint set $\tilde{\mathcal U}_v$}
% \textbf{Initialize: }$\tilde{\mathcal U}_v = \mathcal U_v$, $I = I_0$\;
%  Sample $\{x_i\}_{I_0}$ from $\{B(x)\leq 0\}$\;
%  \While{$\tilde{\mathcal U}_v\neq \emptyset$ or $I\neq \emptyset$}{
%  Set $\tilde I = \{i\in I\; |\; H(x_i, u_v)>-\gamma\}$\;\label{line: h s U}
%   \If{$\tilde I \neq \emptyset $}
%   {
%   $\tilde{\mathcal U}_v = \tilde{\mathcal U}_v\ominus \delta $\; \label{step: Ua reduction}
%   $I = \tilde I$;
%   }
%  }
%  \textbf{Return: }$\bar {\mathcal U}_v$\;
%  \caption{Iterative method for computing $\mathcal U_v$}
% \end{algorithm}

% \begin{Remark}
% Note that if either Algorithm \ref{algo iter c} or \ref{algo: iter U} fails to return a non-empty output (parameter $c$ and the set $\mathcal U_v$, respectively), then the algorithms can be used in conjunction with each other. As an example, Algorithm \ref{algo iter c} can be repeated with a new initialization of $\mathcal U_v$ (obtained using Step \ref{step: Ua reduction} in Algorithm \ref{algo: iter U}), and the process can be repeated until the algorithm returns $c$, or the sets $S_c$ or $\mathcal U_v$ become empty. 
% % , or Algorithm \ref{algo: iter U} can be repeated by sampling the points $\{x_i\}$ from set $S_c$ for some $c>0$ (obtained from Step \ref{step: c increment} in Algorithm \ref{algo iter c}). 
% \end{Remark}






% \textbf{FOLLOWING SECTION IN RED NEEDS MORE DETAILS: SKIP FOR NOW}
% {\color{red}
% \subsubsection{Other approaches} 
% \textit{SOS based construction}
% \cite{wang2018permissive}: assumes the dynamics to be polynomial- setup an SOS and solve for $\tilde h$. 

% \textit{Learning based construction}
% \cite{srinivasan2020synthesis}: online and offline control input synthesis using data-based CBF learning.
% }
% \textbf{Non-attackability margins (local and global), computational (optimization) tools, real-time adjustment}:

% \textbf{Talk about convergence (DoA)}

% Similarly, a subset of the domain of attraction for the convergence property $P_{conv}$ can be computed using Algorithm \ref{algo iter c conv}.

% \begin{algorithm}\label{algo iter c conv}
% \SetAlgoLined
% \KwData{$f,g_v, \mathcal U_v, g_s,\mathcal U_s, V, \delta, \gamma$}
% \KwResult{Parameter $c$}
% \textbf{Initialize: }$c = 0$\;
%  \While{$c \leq \eta$}{
%   Sample $\{x_i\}_{\mathcal I}$ satisfying \eqref{eq: xj xk dist cond} for 2-D (\eqref{eq: xj xk dist cond 3d} for 3D) from $D_c = \{V(x)\leq \eta-c\}$\;\label{line: sampling conv}
%   \eIf{$H_G(x_i, u_v)<-\gamma$ for all $i\in \mathcal I$}{
%   Break\; 
%   }
%   {
%   $c = c+\delta$\;
%   }
%  }
%  \textbf{Return: }$c$\;
%  \caption{Computation of $c$ for convergence}
% \end{algorithm}
% Note that for the sampling in Line \ref{line: sampling conv} of Algorithm \ref{algo iter c conv}, the conditions \eqref{eq: xj xk dist cond} and \eqref{eq: xj xk dist cond 3d} are verified for $d_{D_c}$ instead of $d_{S_c}$.
So far, we presented sufficient conditions to establish the safety of the system \eqref{eq: actual system} under attacks (Proposition \ref{lemma: sufficient conditions non-attack}), a sampling-based method to verify these conditions using a finite number of sampling points (Theorem \ref{thm: sufficient sup H cond}), and iterative methods to compute the set of initial conditions and the input constraint set to satisfy these conditions (Algorithm \ref{algo: iter U c comb}). Thus, in brief, using the results in this section, we can compute the viability domain $S_c$ and control input constraint set $\tilde{\mathcal U}_v\subset\mathcal U_v$, such that for all $x\in S_c$ and $u_v\in \tilde{\mathcal U}_v$, there exists a control input $u_s\in \mathcal U_s$ that can keep the system trajectories in the set $S_c$ at all times. In the next section, we present a method of computing such a control input using a QP formulation.
% , thus, providing the final piece of the solution to Problem \ref{Problem 1}.}


\section{QP based feedback design}\label{sec: QP control}
In this section, we use the sufficient conditions from the previous section to design a feedback law for the system \eqref{eq: actual system} that guarantees security with respect to the safety property under Assumption \ref{assum: d bound}. 
% \subsection{QP based approach}
% For the results in this section, 
We assume that the control input constraint set is given as $\tilde{\mathcal U}\coloneqq\tilde{\mathcal U}_v\times\mathcal U_s =\{v\in \mathbb R^{m}\; |\; u_{j,min}\leq v_j\leq u_{j,max}\}$, i.e., as a box-constraint set where $u_{j,min}< u_{j,max}$ are the lower and upper bounds on the individual control inputs $v_j$ for $j = 1, 2, \ldots, m$, respectively. We can write $\mathcal U$ in a compact form as $\tilde{\mathcal U} = \{v\; |\; A_{u}v\leq b_{u}\}$ where $A_u\in \mathbb R^{2m\times m}, b_u\in \mathbb R^{2m}$. Furthermore, we assume that the system model \eqref{eq: actual system} is control affine, and is of the form:
\begin{align}\label{eq: cont affine}
    \dot x & = f(x) + g_v(s)u_v+g_s(x)u_s + d(t,x),
\end{align}
where $f:\mathbb R^n\rightarrow\mathbb R^n$, $g_v: \mathbb R^n\rightarrow\mathbb R^{n\times m_v}$ and $g_s: \mathbb R^n\rightarrow\mathbb R^{n\times (m-m_v)}$ are continuous functions. In this case, the function $H:\mathbb R^n\times\mathbb R^{m_v}\to\mathbb R$ reads{\small
\begin{align}
    \hspace{-5pt}H(x,u_v) = \hspace{-3pt}\inf_{u_s\in \mathcal U_s}\hspace{-5pt}L_fB(x) + L_{g_s}B(x)u_s +L_{g_v}B(x)u_v.
\end{align}}\normalsize
% Similarly, under the second class of attack on actuators, as described through \eqref{eq: attack model additive attack}, the special case of the control affine model takes the following form:
% \begin{align}\label{eq: NL pert cont affine  additive attack}
%     \dot x(t) & = f(x(t)) + \begin{bmatrix}g(x(t)) &  g(x(t))\end{bmatrix}\begin{bmatrix}u(t) \\ \tilde u_v(t)\end{bmatrix},
% \end{align}
% and the function $H$ reads
% \begin{align}
%     H(x,u_v) = \inf_{u\in \mathcal U\ominus \tilde{\mathcal U}_v}L_fB(x) + L_{g}B(x)u +L_gh_{S}(x)\tilde u_v.
% \end{align}
% \normalsize 
In addition to the safety requirement in Problem \ref{Problem 1}, we impose the requirement of convergence of the system trajectories of \eqref{eq: cont affine} to the origin. To this end, given a twice continuously differentiable, positive definite function $V:\mathbb R^n\rightarrow \mathbb R_+$ as a candidate Lyapunov function, we use the condition 
\begin{align}
   \hspace{-10pt}L_fV(x) + L_{g_s}V(x)u_s+L_{g_v}V(x)u_v \leq -\zeta V(x) - l_V \delta,
\end{align}
where $\zeta>0$, to guarantee convergence of the system trajectories to the origin under $d$ satisfying Assumption \ref{assum: d bound}. We assume that the set $S$ is an $(n-1)$-unit sphere, so that we can use the results from the previous section to compute a viability domain for it, and that $0\in \textnormal{int}(S)$, so that the convergence requirement is feasible. The linear constraints on the control input, and the system model being control affine, helps us formulate a convex optimization problem that can be efficiently solved for real-time control synthesis \cite{ames2017control}. We propose the following Quadratic Program (QP) to solve Problem \ref{Problem 1}. 
% where the objective is to minimize the norm of the control input \cite{garg2019prescribedTAC}. 
Define $z =(v_s, v_v, \eta, \zeta)\in \mathbb R^{m+2}$ and for a given $x\in \mathbb R^n$, consider the following {QP}:\vspace{-10pt}

\small{
\begin{subequations}\label{QP gen}
\begin{align}
\hspace{10pt}\min_{z} \quad \frac{1}{2}|z|^2 + q\zeta\\
    \textrm{s.t.} \;\quad \; \; A_uv_{na}  \leq &  \; b_u, \label{C1 cont const}\\
    % L_fV(x) + L_gV(x)v  \leq & \; \delta_1V(x)-\alpha V(x)^{\gamma_1}\nonumber\\
    % & -\alpha V(x)^{\gamma_2} -l_G\delta,\label{C2 stab const}\\
    L_fB(x) + L_{g_s}B(x)v_s \leq & -\eta ~(B(x)+c)\nonumber \\
    & -\sup_{u_v\in \tilde{\mathcal U}_v}L_{g_v}B(x)u_v-l_B\delta,\label{C3 safe const}\\
     L_fV(x) + L_{g_s}V(x)v_s  + & L_{g_v}V(x)v_v\leq  -\zeta ~ V(x) -l_V\delta,\label{C4 conv const}
    % \\
    % \frac{2}{T_{ud}}\leq \alpha_1(\gamma_1-1) \leq &  \alpha_2(1-\gamma_2)\label{C4 T const}, 
    % \frac{\mu\pi}{2T_{ud}}\leq & \alpha_1, \label{C4 T const}\\  \frac{\mu\pi}{2T_{ud}}\leq & \alpha_2, \label{C4 T const2}
\end{align}
\end{subequations}}\normalsize
where $q>0$ is a constant, $l_B, l_v$ are the Lipschitz constants of the functions $B$ and $V$, respectively, and $c$ and $\tilde{\mathcal U}_v$ are the output of Algorithm \ref{algo: iter U c comb}. Here, $\eta$ and $\zeta$ are slack variables used for guaranteeing feasibility of the QP (see \cite[Lemma 6]{garg2019prescribedTAC}). The first constraint \eqref{C1 cont const} is the input constraints, the second constraint is the CBF condition from Lemma \ref{lemma: nec suff safety} for forward invariance of the set $S_c$ and the third constraint \eqref{C4 conv const} is CLF constraint for convergence of the system trajectories to the origin. Note that the secure input $v_s$ is used in both \eqref{C3 safe const} and \eqref{C4 conv const}, while the vulnerable input $v_v$ is only used in \eqref{C4 conv const}. 
% The parameters $\alpha, \alpha, \gamma_1, \gamma_2$ are fixed, and are chosen as $\alpha = \frac{\mu\pi}{2T_{ud}}$, $\gamma_1 = 1+\frac{1}{\mu}$ and $\gamma_2 = 1-\frac{1}{\mu}$ with $\mu>1$. 

Let the optimal solution of \eqref{QP gen} at a given point $x\in \mathbb R^n$ be denoted as $z^*(x) = (v_s^*(x), v_v^*(x), \eta^*(x),\zeta^*(x))$. In order to guarantee continuity of the solution $z^*$ with respect to $x$, we need to impose the strict complementary slackness condition on \eqref{QP gen} (see \cite{garg2019prescribedTAC}). In brief, if the $i-$the constraint of \eqref{QP gen}, with $i \in \{1, 2, 3\}$, is written as $G_i(x,z)\leq 0$, and the corresponding Lagrange multiplier is $\lambda_i\in \mathbb R_+$, then strict complementary slackness requires that $\lambda_i^*G(x,z^*)<0$, where $z^*, \lambda_i^*$ denote the optimal solution and the corresponding optimal Lagrange multiplier, respectively. We are now ready to state the following result.  

% \begin{Theorem}
% Let $c_1$ and $c_2$ be the output of the Algorithms \ref{algo iter c} and Algorithm \ref{algo iter c conv} corresponding to the functions $H_s$ and $H_G$ for the system \eqref{eq: NL pert cont affine} (respectively, \eqref{eq: NL pert cont affine  additive attack}), and assume that there exists a control input $u_s$ such that the sets $S_c = \{x\; |\; B(x)\leq -c_1\}$ and $D_c =  \{x\; |\; B(x)\leq \eta-c_2\}$ forward-invariant for the model \eqref{eq: NL pert cont affine} (respectively, \eqref{eq: NL pert cont affine  additive attack}). Then, the QP \eqref{QP gen} is feasible for all $x\in S_c\cap D_c$ and the control input $u = v^*$, where $v^*$ is the solution of the QP \eqref{QP gen} leads to security of \eqref{eq: actual system} for safety and convergence properties under an attack of the form \eqref{eq: model} (respectively, \eqref{eq: attack model additive attack}).
% \end{Theorem}

\begin{Theorem}
Given the functions $F, d, B, V$ and the attack model \eqref{eq: attack model}, suppose Assumptions \ref{assum: d bound}-\ref{assum: max dist tring nD} hold. Let $c$ and $\tilde{\mathcal U}_v$ be the output of the Algorithm \ref{algo: iter U c comb}. Assume that the strict complementary slackness holds for the QP \eqref{QP gen} for all $x\in S_c$. Then, the QP \eqref{QP gen} is feasible for all $x\in S_c$, and the control law defined as $k_s(x) = v_s^*(x)$ is continuous on $\textnormal{int}(S_c)$, and solves Problem \ref{Problem 1} for all $x(0)\in X_0\coloneqq  \textnormal{int}(S_c)$.
% i.e., the resulting closed-loop system $\mathcal S$ satisfies $[\mathcal A_\tau]\mathcal S\models P_{safe, \textnormal{int}(S_c)}$ for all $\tau\geq 0$. 
\end{Theorem}

\begin{proof}
% The proof is based on the results in \cite{garg2019prescribedTAC}.
Per Theorem \ref{thm: sufficient sup H cond}, the set $S_c$ is a viability domain for the system \eqref{eq: cont affine} under Assumption \ref{assum: LC F del B}. Thus, feasibility of the QP \eqref{QP gen} follows from \cite[Lemma 6]{garg2019prescribedTAC}. Note also that with $V$ being twice continuously differentiable and under Assumption \ref{assum: LC F del B}, the Lie derivatives of the functions $V$ and $B$ along $f, g_s$, and $g_v$ are continuous. Thus, per \cite[Theorem 1]{garg2019prescribedTAC}, the solution $z^*$ of the QP \eqref{QP gen} is continuous on $\textnormal{int}(S_c)$. Finally, since the set $S_c$ is compact, it follows from \cite[Lemma 7]{garg2019prescribedTAC} that the closed-loop trajectories are uniquely defined for all $t\geq 0$. Uniqueness of the closed-loop trajectories, Assumption \ref{assum: d bound} and feasibility of the QP \eqref{QP gen} for all $x\in S_c$ implies that all the conditions of Lemma \ref{lemma: nec suff safety} are satisfied and it follows that the set $S_c$ is forward invariant for the system \eqref{eq: cont affine}. 
% , i.e., the closed-loop system $\mathcal S$ satisfies $[\mathcal A_\tau]S\models P_{safe, \textnormal{int}(S_c)}$ for all $\tau\geq 0$.
\end{proof}

{
\begin{Remark}
In this work, only the control input $u_s$ is used to achieve safety since it is unknown when the vulnerable input $u_v$ comes under an attack. This conservative assumption can be relaxed by utilizing an attack-detection mechanism, which can trigger a switching mechanism from a \textnormal{nominal} control design, assuming no attacks, to the proposed method under an attack. We leave this detection-based switching mechanism as part of our future work.
\end{Remark}
}

% \subsection{Non-attackability margin}
% Using the ideas from the results in the previous section, we can define the notion of non-attackability margin for safety as:

% \begin{Definition}
% The function $m_S:\mathbb R\times \mathbb R^n\rightarrow\mathbb R$, defined as
% \begin{align}
%     m_S(\gamma, x) = \sup_{u_v\in \mathcal U_v}H(x,u_v) + \gamma,
% \end{align}
% is called as local Non-Attackability Margin (NAM) for safety at a point $x\in S$. The global NAM, $\bar m_S(\gamma)$, is defined as $\bar m_S(\gamma) = \sup_{x\in S}m_S(\gamma, x)$.  
% \end{Definition}

% Similarly, we can define the notion of non-attackability margin for fixed-time convergence as follows: 

% \begin{Definition}
% The function $m_G:\mathbb R\times \mathbb R^n\rightarrow\mathbb R$, defined as
% \begin{align}
%     m_G(\gamma, x) = & \sup_{u_v\in \mathcal U_v}H_G(x,u_v)+\gamma,
% \end{align}
% is called as local NAM for convergence at a point $x\in K$. The global NAM, $\bar m_G(\gamma)$ is defined as $\bar m_G(\gamma) = \sup_{x\in K}m_S(\gamma, x)$.  
% \end{Definition}


% The local NAM $m(\gamma,x)$ quantifies how susceptible the closed-loop system is to an attack on the inputs. In particular, larger value of $m_S(\gamma,x)$ or $m_G(\gamma, x)$ implies higher susceptibility of the system's safety or convergence, respectively, at a point $x$. In particular, if $\bar m_S(\gamma)>0$ and $\bar m_G(\gamma)>0$ for all $\gamma> 0$, then it is not possible to guarantee that the system is invulnerable.  

% \begin{figure}[t]
% 	\centering
% 	\includegraphics[width=0.7\columnwidth,clip]{sphere_mesh.eps}
% 	\caption{Triangulation on the surface of the unit sphere with 400 sample points.}
% 	\label{fig: sphere mesh}
% \end{figure}

% \alvaro{Not sure I understand what is the goal of this section. Isn't the control action already fixed? I guess this is a control action that will help us find the initial set and the actuator bounds?}


\section{Numerical Experiments}
% \subsection{3D Linear-Time Invariant system example}
To showcase the effectiveness of the proposed method, we present an academic example with the system given as 
\begin{align}
    \dot x = f(x) + Ax + Bu + d(t,x),
\end{align}
where $A\in \mathbb R^{3\times 3}$ and $B\in \mathbb R^{3\times 2}$. The input constraint sets are $\mathcal U_1 = \{u_1\in \mathbb R\; |\; |u_1|\leq u_{M1}\}$ and $\mathcal U_2 = \{u_2\in \mathbb R\; |\; |u_2|\leq u_{M2}\}$ for some $u_{M1}, u_{M2}>0$. The safe set is $S = \{x\in \mathbb R^3\; |\; |x|^2-1\leq 0\}$ corresponding to the function $h(x) = |x|^2-1$, i.e., the safe set is the unit sphere. We use randomly generated matrices $A$ and $B$ such that the pairs $(A,B_1)$ and $(A, B_2)$ are controllable, where $B_1$ and $B_2$ are the first and the second columns of the matrix $B$, respectively. The matrices $(A,B)$ and the function $f$ are

{\footnotesize
\begin{align*}
    A \!=\!\begin{bmatrix}0.61  & \hspace{-12pt} 0.37 & \hspace{-12pt} 2.69\\
    -0.06& \hspace{-12pt} -1.02 & \hspace{-12pt} -0.88\\
    1.33& \hspace{-12pt} -2.71& \hspace{-12pt} 0.91\end{bmatrix}\!, B\!=\! \begin{bmatrix}-0.24 & \hspace{-10pt} 0.04\\
    0.32 & \hspace{-10pt} -0.01\\
    -1.12& \hspace{-10pt}-0.07\end{bmatrix}\!, f(x) \!=\! 0.01\!\begin{bmatrix}x_1^3 + x_2^2x_3\\ x_2^3 + x_3^2x_1\\x_3^3 + x_1^2x_2 \end{bmatrix}.
\end{align*}}\normalsize
% \begin{align*}
% \end{align*}

\begin{figure}[b]
\vspace{-10pt}
	\centering
	\includegraphics[width=\columnwidth,clip]{sup_H_figure.eps}
	\caption{The value of $\max_i\sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v) +l_Hd_a +l_B\delta+l_Hd_a$ and the number of sampling points for different values of $d_a$.}
	\label{fig:sup H}
\end{figure}
We use MATLAB code from \cite{anton2021SamplingCode} to generate a uniform sampling on the boundary of the unit sphere.
% , as shown in Figure \ref{fig: sphere mesh}. 
Figure \ref{fig:sup H} shows the maximum value of $\sup_{u_v\in \tilde{\mathcal U}_v}H(\bar x,u_v)+l_Hd_a +l_B\delta$ over the sampling points for different values of $d_a$. It is observed that condition \eqref{eq: sup H cond 3D} is satisfied when $d_a =0.0406$, and the corresponding number of sampling points is $N_p = 3062$. 
% \begin{figure}[b]
% 	\centering
% 	\includegraphics[width=0.9\columnwidth,clip]{h_plot_ex1_case0.eps}
% 	\caption{Evolution of the function $h$ with time.}
% 	\label{fig:ex1case1 h func}
% \end{figure}
% \begin{figure}[t]
% 	\centering
% 	\includegraphics[width=0.9\columnwidth,clip]{u_plot_ex1_case0.eps}
% 	\caption{vulnerable input $u_1$ and the control input $u_2$ with time.}
% 	\label{fig:ex1case1 input}
% \end{figure}
% \begin{figure}[t]
% 	\centering
% 	\includegraphics[width=1\columnwidth,clip]{h_plot_ex1_case0_1.eps}
% 	\caption{Evolution of the function $h$ with time.}
% 	\label{fig:ex1 h func}
% \end{figure}
Without loss of generality, we assume that $u_2$ is vulnerable.


\begin{figure}[t]
	\centering
	\includegraphics[width=0.95\columnwidth,clip]{uh_plot_20_15_NL.eps}
	\caption{The vulnerable input $u_v$ and the function $h$ under attacks 1 and 2.}
\vspace{-10pt}
	\label{fig:ex1 uh func 10 5}
\end{figure}
\begin{figure}[t]
	\centering
	\includegraphics[width=0.95\columnwidth,clip]{traj_plot_20_15_NL.eps}
	\caption{The closed-loop paths traced by the system under attacks 1 and 2. 
% 	The top figure of is a 3D plot, while the rest of the figures are projections on $x_1-x_2, x_1-x_3$ and $x_2-x_3$ planes.
	}
\vspace{-20pt}
	\label{fig:ex1 traj 10 5}
\end{figure}

\noindent We use Algorithm \ref{algo: iter U c comb} to compute the set $\tilde{\mathcal U}_i$ and a value of $c$ such that \eqref{eq: sup H cond 3D} holds for all the sampling points. With $u_{M1} = 20$ and $u_{M2} = 20$ (defining the sets $\mathcal U_s, \mathcal U_v$), Algorithm \ref{algo: iter U c comb} gives $c = 0$ for the viability domain $\{x\; |\; h(x)\leq c\}$ and $\tilde u_{M2} = 7.5$ (defining the set $\tilde{\mathcal U}_v$) as the feasible bound on the attack signal $u_2$. The attack happens at a randomly chosen $\tau = 0.436$ and $\delta = 0.1$ in Assumption \ref{assum: d bound}. 
% {\footnotesize
% \begin{align*}
%     A = \begin{bmatrix}0.4154 & 0.0683 & -0.4019\\
%     0.5773  &  -0.4196  &  0.8921\\
%     0.5684  & -0.1941  &  1.2891\end{bmatrix}, B = \begin{bmatrix}4.5121  & -8.5832\\
%     2.5132 & -10.0804\\
%   -12.1319  &  7.1836\end{bmatrix}
% \end{align*}}\normalsize
% with 



First, we illustrate that the system violates safety when the attack signal $u_2$ does not satisfy the bounds computed by Algorithm \ref{algo: iter U c comb}. Figure \ref{fig:ex1 uh func 10 5} shows the vulnerable input $u_v$ for the initial two attack scenarios (Attack 1 and 2) where $\bar u_{M2} = 20$ and $\bar u_{M2} = 15$, i.e., the set $\tilde{\mathcal U}_v$ is larger than the one computed using the proposed algorithm. Figure \ref{fig:ex1 uh func 10 5} also plots the evolution of the barrier function $h$ with time for the two cases. It can be observed that the function $h$ corresponding to this attack takes positive values, and thus, the safety property for the system is violated. Figure \ref{fig:ex1 traj 10 5} plots the corresponding closed-loops paths for the two scenarios, and it can be seen that the system leaves the safe set, thus violating safety. 

In the rest of the attack scenarios (Attack 3-6), the bound $|u_v|\leq 7.5$ is imposed as computed by the proposed algorithm.  Figure \ref{fig:ex1 uh func rest} plots the different types of attack signals used in these scenarios, namely, saturated signals with $u_v = 7.5$ and $u_v = -7.5$, square wave and sinusoidal signal, both with amplitude $7.5$. The corresponding evolution of the barrier function $h$ illustrates that the system maintains safety in all four scenarios. Figure \ref{fig:ex1 traj rest} plots the closed-loops paths for these attack scenarios, and it can be seen that the system trajectories evolve in the safe set at all times, thus maintaining safety. 
%Finally, to illustrate the effect of an attack on systems' performance, we simulated without any attacks. Figure \ref{fig: V plot} plots the function $V(x) = \frac{1}{2}|x|^2$ for all the attack scenarios as well as when there is no attack on $u_v$. It can be seen that the value of the function $V$ under an attack is higher than the case when there is no attack, illustrating that an attack on the system input $u_v$ can deteriorate its performance. 
% Another line of future work is an initial characterization of a class of systems where our tools are applicable and others where it fails (where there are no bounds that can prevent successful attacks). 
%In this work, we assumed that the time when the vulnerable input can be attacked is unknown. Future work involves devising an attack-detection mechanism and switching controller to propose more efficient controllers.
Through this case study, we illustrate that if the system parameters are not chosen according to our proposed method, then there might exist attacks that can lead to violation of safety. On the other hand, when the system parameters are designed according to the proposed algorithm, no attack can violate safety, confirming that the system is secure by design. 
%, and it can be observed that $h(x(t))\leq 0$ for all $t\geq 0$ in both cases, implying that the system trajectories evolve in the safe set at all times. Figure \ref{fig:ex1 input} plots the input and vulnerable input for the two cases, and it can be seen that the inputs satisfy the imposed bounds in both cases. 

\begin{figure}[t]
	\centering
	\includegraphics[width=0.95\columnwidth,clip]{uh_plot_rest_NL.eps}
	\caption{The vulnerable input $u_v$ and the function $h$ under attacks 3-6.}
\vspace{-10pt}
	\label{fig:ex1 uh func rest}
\end{figure}
\begin{figure}[t]
	\centering
	\includegraphics[width=0.95\columnwidth,clip]{traj_plot_rest_NL.eps}
	\caption{The closed-loop paths traced by the system under attacks 3-6. 
% 	The top figure of is a 3D plot, while the rest of the figures are projections on $x_1-x_2, x_1-x_3$ and $x_2-x_3$ planes. 
	}
\vspace{-20pt}
	\label{fig:ex1 traj rest}
\end{figure}



%\begin{figure}[t]
%	\centering
%	\includegraphics[width=1\columnwidth,clip]{V_plot.eps}
%	\caption{The value of function $V(x) = \frac{1}{2}|x|^2$ with time under no attack and all the attack scenarios 1-6.}
%	\label{fig: V plot}
%\end{figure}



% \begin{figure}[t]
% 	\centering
% 	\includegraphics[width=1\columnwidth,clip]{u_plot_ex1_case0_1.eps}
% 	\caption{Control input $u_1$ and the vulnerable input $u_2$ with time.}
% 	\label{fig:ex1 input}
% \end{figure}

% \begin{figure}[t]
% 	\centering
% 	\includegraphics[width=1\columnwidth,clip]{u_plot_ex1_u2_sin_dist_0_2.eps}
% 	\caption{Evolution of the function $h$, input $u_1$ and the vulnerable input $u_2$ with time for $\delta = 0.2$.}
% 	\label{fig:ex1 sin attack}
% \end{figure}


% \alvaro{I think we need more insights into how our design is protecting the system a priori. First, we should show that an attack can drive the system to an unsafe space if the vulnerable input does not satisfy the computed constraints.  The plots should show how the attack drives the system to this unsafe space. Then we can show how with our constraints, the attacker cannot reach the unsafe space and show this under a variety of attacks on u (replay attacks, sinusoidal, random, etc.) }

% \subsection{Quadruple tank process}
% As mentioned in \cite{giraldo2020daria}, the quadruple tank process, first introduced in \cite{johansson2000quadruple}, is one of the benchmark problems in cyber-security for control systems. In the interest of space, we refer the reader to \cite{johansson2000quadruple} for a detailed description of the problem. Here, we present the system dynamics of the coupled tank problem:
% % \begin{align}
% %     \dot x = Ax + Bu,
% % \end{align}
% % where $x = \begin{bmatrix}
% % x_1 \\ x_2 \\ x_3 \\ x_4
% % \end{bmatrix}$,  $
% % A = \begin{bmatrix}
% % -\frac{1}{T_1} & 0 & \frac{A_3}{A_1T_3} & 0\\ 
% % 0 & -\frac{1}{T_2} & 0 & \frac{A_4}{A_2T_4}\\
% % 0 & 0 & -\frac{1}{T_3} & 0\\
% % 0 & 0 & 0 & -\frac{1}{T_4}
% % \end{bmatrix} $ $B = \begin{bmatrix}
% % \frac{\rho_1k_1}{A_1} & 0 \\ 0 & \frac{\rho_2 k_2}{A_2} \\ 0 & \frac{(1-\rho_2)k_2}{A_3} \\ \frac{(1-\rho_1)k_1}{A_4}
% % \end{bmatrix}$, and $ u = \begin{bmatrix}
% % u_1\\ u_2
% % \end{bmatrix}$.
% \begin{subequations}
% \begin{align}
%     \dot h_1 = & -\frac{a_1}{A_1}\sqrt{2gh_1}+\frac{a_3}{A_1}\sqrt{2gh_3} +\frac{\gamma_1k_1}{A_1}v_1,\\
%     \dot h_2 = & -\frac{a_2}{A_2}\sqrt{2gh_2}+\frac{a_4}{A_2}\sqrt{2gh_4} +\frac{\gamma_2k_2}{A_2}v_2.\\
%     \dot h_3 = & -\frac{a_3}{A_3}\sqrt{2gh_3}+\frac{(1-\gamma_2)k_2}{A_3}v_2,\\
%     \dot h_4 = & -\frac{a_4}{A_4}\sqrt{2gh_4}+\frac{(1-\gamma_1)k_1}{A_4}v_1,
% \end{align}
% \end{subequations}
% where $h_i$ is the output voltage corresponding to the water level of the $i-$th tank, $v_1, v_2$ are the input voltages, and $g, a_i, A_, \gamma_i, k_i>0$ some given constants (see Figure \ref{fig:4 tank problem}). 

% \begin{figure}[t]
% 	\centering
% 	\includegraphics[width=0.9\columnwidth,clip]{4_tank_image.PNG}
% 	\caption{Quadruple tank problem.}
% 	\label{fig:4 tank problem}
% \end{figure}


\section{Conclusion and Future Work}
{In this paper, we study the problem of computing a viability domain and input constraint set so that the safety of a system can be guaranteed under attacks on the system inputs. In contrast to prior work on the computation of viability domain whose applicability is limited to linear or polynomial dynamics or whose computational complexity grows exponentially with system dimension, our method is computationally efficient and applies to a general class of nonlinear systems. We showed that when the system parameters are chosen using our sampling-based iterative algorithm, the resulting system is resilient to arbitrary attacks, and thus, is secure by design.}
% \textbf{Discussion and Future Work:} 


Our approach can be used to design bounds (that can either be implemented physically or in a tamper-proof reference monitor) that will prevent attackers from driving control systems to unsafe states. It is efficient (sampling-based viability computation) and general (applicable to non-linear systems).
% This line of work opens up several new problems that we will consider in future work, such as the operational impact of the proposed strategy. 
By limiting the range of actuation and the initial set, we are limiting the responsiveness of control action, and in general, systems with our defense might converge slower to the desired set point or trajectory. One way to mitigate this is to use attack-detection mechanisms and switching strategy so that more efficient controllers can be used when the system is not under an attack. 
% We considered systems modeled under a general class of nonlinear dynamics; thus, the proposed results can be used for a large class of real-world systems. Then, we showed that it is possible to design computationally tractable iterative algorithms to compute viability domain for 2D and 3D systems. Finally, we showed that the computed viability domain could be used in a provably feasible QP formulation for the real-time synthesis of feedback law.


\bibliographystyle{IEEEtran}
\bibliography{myreferences}

\end{document}
% Generated by IEEEtran.bst, version: 1.14 (2015/08/26)
\begin{thebibliography}{10}
\providecommand{\url}[1]{#1}
\csname url@samestyle\endcsname
\providecommand{\newblock}{\relax}
\providecommand{\bibinfo}[2]{#2}
\providecommand{\BIBentrySTDinterwordspacing}{\spaceskip=0pt\relax}
\providecommand{\BIBentryALTinterwordstretchfactor}{4}
\providecommand{\BIBentryALTinterwordspacing}{\spaceskip=\fontdimen2\font plus
\BIBentryALTinterwordstretchfactor\fontdimen3\font minus
  \fontdimen4\font\relax}
\providecommand{\BIBforeignlanguage}[2]{{%
\expandafter\ifx\csname l@#1\endcsname\relax
\typeout{** WARNING: IEEEtran.bst: No hyphenation pattern has been}%
\typeout{** loaded for the language `#1'. Using the pattern for}%
\typeout{** the default language instead.}%
\else
\language=\csname l@#1\endcsname
\fi
#2}}
\providecommand{\BIBdecl}{\relax}
\BIBdecl

\bibitem{lee2014german}
R.~M. Lee, M.~J. Assante, and T.~Conway, ``German steel mill cyber attack,''
  \emph{Industrial Control Systems}, vol.~30, p.~62, 2014.

\bibitem{oueslati2019comparative}
N.~E. Oueslati, H.~Mrabet, A.~Jemai, and A.~Alhomoud, ``Comparative study of
  the common cyber-physical attacks in industry 4.0,'' in \emph{2019
  International Conference on Internet of Things, Embedded Systems and
  Communications}.\hskip 1em plus 0.5em minus 0.4em\relax IEEE, 2019, pp. 1--7.

\bibitem{cardenascyber}
\BIBentryALTinterwordspacing
A.~Cardenas, ``Cyber-physical systems security knowledge area issue.'' {T}he
  Cyber Security Body Of Knowledge. [Online]. Available:
  \url{https://www.cybok.org/media/downloads/Cyber-Physical_Systems_Security_issue_1.0.pdf}
\BIBentrySTDinterwordspacing

\bibitem{choi2018detecting}
H.~Choi, W.-C. Lee, Y.~Aafer, F.~Fei, Z.~Tu, X.~Zhang, D.~Xu, and X.~Deng,
  ``Detecting attacks against robotic vehicles: A control invariant approach,''
  in \emph{Proceedings of the 2018 ACM SIGSAC Conference on Computer and
  Communications Security}, 2018, pp. 801--816.

\bibitem{renganathan2020distributionally}
V.~Renganathan, N.~Hashemi, J.~Ruths, and T.~H. Summers, ``Distributionally
  robust tuning of anomaly detectors in cyber-physical systems with stealthy
  attacks,'' in \emph{2020 American Control Conference (ACC)}.\hskip 1em plus
  0.5em minus 0.4em\relax IEEE, 2020, pp. 1247--1252.

\bibitem{urbina2016limiting}
D.~I. Urbina, J.~A. Giraldo, A.~A. Cardenas, N.~O. Tippenhauer, J.~Valente,
  M.~Faisal, J.~Ruths, R.~Candell, and H.~Sandberg, ``Limiting the impact of
  stealthy attacks on industrial control systems,'' in \emph{Proceedings of the
  2016 ACM SIGSAC conference on computer and communications security}, 2016,
  pp. 1092--1105.

\bibitem{cardenas2006framework}
A.~A. C{\'a}rdenas, J.~S. Baras, and K.~Seamon, ``A framework for the
  evaluation of intrusion detection systems,'' in \emph{2006 IEEE Symposium on
  Security and Privacy (S\&P'06)}.\hskip 1em plus 0.5em minus 0.4em\relax IEEE,
  2006, pp. 15--pp.

\bibitem{al2018cyber}
M.~N. Al-Mhiqani, R.~Ahmad, W.~Yassin, A.~Hassan, Z.~Z. Abidin, N.~S. Ali, and
  K.~H. Abdulkareem, ``Cyber-security incidents: a review cases in
  cyber-physical systems,'' \emph{Int. J. Adv. Comput. Sci. Appl}, no.~1, pp.
  499--508, 2018.

\bibitem{ames2017control}
A.~D. Ames, X.~Xu, J.~W. Grizzle, and P.~Tabuada, ``Control barrier function
  based quadratic programs for safety critical systems,'' \emph{IEEE
  Transactions on Automatic Control}, vol.~62, no.~8, pp. 3861--3876, 2017.

\bibitem{wang2018permissive}
L.~Wang, D.~Han, and M.~Egerstedt, ``Permissive barrier certificates for safe
  stabilization using sum-of-squares,'' in \emph{2018 Annual American Control
  Conference (ACC)}.\hskip 1em plus 0.5em minus 0.4em\relax IEEE, 2018, pp.
  585--590.

\bibitem{choi2021robust}
J.~J. Choi, D.~Lee, K.~Sreenath, C.~J. Tomlin, and S.~L. Herbert, ``Robust
  control barrier-value functions for safety-critical control,'' \emph{arXiv
  preprint arXiv:2104.02808}, 2021.

\bibitem{giraldo2020daria}
J.~Giraldo, S.~H. Kafash, J.~Ruths, and A.~A. Cardenas, ``Daria: Designing
  actuators to resist arbitrary attacks against cyber-physical systems,'' in
  \emph{2020 IEEE European Symposium on Security and Privacy (EuroS\&P)}.\hskip
  1em plus 0.5em minus 0.4em\relax IEEE, 2020, pp. 339--353.

\bibitem{erlingsson2004inlined}
U.~Erlingsson, \emph{The inlined reference monitor approach to security policy
  enforcement}.\hskip 1em plus 0.5em minus 0.4em\relax Cornell University,
  2004.

\bibitem{pasqualetti2013attack}
F.~Pasqualetti, F.~D{\"o}rfler, and F.~Bullo, ``Attack detection and
  identification in cyber-physical systems,'' \emph{IEEE transactions on
  automatic control}, vol.~58, no.~11, pp. 2715--2729, 2013.

\bibitem{kafash2018constraining}
S.~H. Kafash, J.~Giraldo, C.~Murguia, A.~A. Cardenas, and J.~Ruths,
  ``Constraining attacker capabilities through actuator saturation,'' in
  \emph{2018 Annual American Control Conference}.\hskip 1em plus 0.5em minus
  0.4em\relax IEEE, 2018, pp. 986--991.

\bibitem{clarke2008nonsmooth}
F.~H. Clarke, Y.~S. Ledyaev, R.~J. Stern, and P.~R. Wolenski, \emph{Nonsmooth
  analysis and control theory}.\hskip 1em plus 0.5em minus 0.4em\relax Springer
  Science \& Business Media, 2008, vol. 178.

\bibitem{blanchini1999set}
F.~Blanchini, ``Set invariance in control,'' \emph{Automatica}, vol.~35,
  no.~11, pp. 1747--1767, 1999.

\bibitem{garg2021robust}
K.~Garg and D.~Panagou, ``Robust control barrier and control lyapunov functions
  with fixed-time convergence guarantees,'' in \emph{2021 American Control
  Conference (ACC)}, 2021, pp. 2292--2297.

\bibitem{oudot2003provably}
S.~Oudot and J.-D. Boissonnat, ``Provably good surface sampling and
  approximation.'' in \emph{Symposium on Geometry Processing}, 2003, pp. 9--18.

\bibitem{leopardi2009diameter}
P.~Leopardi, ``Diameter bounds for equal area partitions of the unit sphere,''
  \emph{Electron. Trans. Numer. Anal}, vol.~35, pp. 1--16, 2009.

\bibitem{de1997computational}
M.~De~Berg, M.~Van~Kreveld, M.~Overmars, and O.~Schwarzkopf, ``Computational
  geometry,'' in \emph{Computational geometry}.\hskip 1em plus 0.5em minus
  0.4em\relax Springer, 1997, pp. 1--17.

\bibitem{bansal2017hamilton}
S.~Bansal, M.~Chen, S.~Herbert, and C.~J. Tomlin, ``Hamilton-jacobi
  reachability: A brief overview and recent advances,'' in \emph{IEEE 56th
  Conference on Decision and Control}.\hskip 1em plus 0.5em minus 0.4em\relax
  IEEE, 2017, pp. 2242--2253.

\bibitem{garg2019prescribedTAC}
K.~Garg, E.~Arabi, and D.~Panagou, ``Fixed-time control under spatiotemporal
  and input constraints: A {Q}{P} based approach,'' \emph{arXiv preprint
  arXiv:1906.10091}, 2019.

\bibitem{anton2021SamplingCode}
\BIBentryALTinterwordspacing
A.~Semechko, ``Suite of functions to perform uniform sampling of a sphere,''
  gitHub. Retrieved August 24, 2021. [Online]. Available:
  \url{https://github.com/AntonSemechko/S2-Sampling-Toolbox}
\BIBentrySTDinterwordspacing

\end{thebibliography}