Augmented Symbolic Execution for Information Flow in Hardware Designs
Extracted source text · arXiv 2307.11884
%% bare_conf_compsoc.tex
%% V1.4b
%% 2015/08/26
%% by Michael Shell
%% See:
%% http://www.michaelshell.org/
%% for current contact information.
%%
%% This is a skeleton file demonstrating the use of IEEEtran.cls
%% (requires IEEEtran.cls version 1.8b or later) with an IEEE Computer
%% Society conference paper.
%%
%% Support sites:
%% http://www.michaelshell.org/tex/ieeetran/
%% http://www.ctan.org/pkg/ieeetran
%% and
%% http://www.ieee.org/
%%*************************************************************************
%% Legal Notice:
%% This code is offered as-is without any warranty either expressed or
%% implied; without even the implied warranty of MERCHANTABILITY or
%% FITNESS FOR A PARTICULAR PURPOSE!
%% User assumes all risk.
%% In no event shall the IEEE or any contributor to this code be liable for
%% any damages or losses, including, but not limited to, incidental,
%% consequential, or any other damages, resulting from the use or misuse
%% of any information contained here.
%%
%% All comments are the opinions of their respective authors and are not
%% necessarily endorsed by the IEEE.
%%
%% This work is distributed under the LaTeX Project Public License (LPPL)
%% ( http://www.latex-project.org/ ) version 1.3, and may be freely used,
%% distributed and modified. A copy of the LPPL, version 1.3, is included
%% in the base LaTeX documentation of all distributions of LaTeX released
%% 2003/12/01 or later.
%% Retain all contribution notices and credits.
%% ** Modified files should be clearly indicated as such, including **
%% ** renaming them and changing author support contact information. **
%%*************************************************************************
% *** Authors should verify (and, if needed, correct) their LaTeX system ***
% *** with the testflow diagnostic prior to trusting their LaTeX platform ***
% *** with production work. The IEEE's font choices and paper sizes can ***
% *** trigger bugs that do not appear when using other class files. *** ***
% The testflow support page is at:
% http://www.michaelshell.org/tex/testflow/
\documentclass[conference,compsoc]{IEEEtran}
% Some/most Computer Society conferences require the compsoc mode option,
% but others may want the standard conference format.
%
% If IEEEtran.cls has not been installed into the LaTeX system files,
% manually specify the path to it like:
% \documentclass[conference,compsoc]{../sty/IEEEtran}
% Some very useful LaTeX packages include:
% (uncomment the ones you want to load)
% *** MISC UTILITY PACKAGES ***
%
%\usepackage{ifpdf}
% Heiko Oberdiek's ifpdf.sty is very useful if you need conditional
% compilation based on whether the output is pdf or dvi.
% usage:
% \ifpdf
% % pdf code
% \else
% % dvi code
% \fi
% The latest version of ifpdf.sty can be obtained from:
% http://www.ctan.org/pkg/ifpdf
% Also, note that IEEEtran.cls V1.7 and later provides a builtin
% \ifCLASSINFOpdf conditional that works the same way.
% When switching from latex to pdflatex and vice-versa, the compiler may
% have to be run twice to clear warning/error messages.
% *** CITATION PACKAGES ***
%
\ifCLASSOPTIONcompsoc
% IEEE Computer Society needs nocompress option
% requires cite.sty v4.0 or later (November 2003)
\usepackage[nocompress]{cite}
\else
% normal IEEE
\usepackage{cite}
\fi
% cite.sty was written by Donald Arseneau
% V1.6 and later of IEEEtran pre-defines the format of the cite.sty package
% \cite{} output to follow that of the IEEE. Loading the cite package will
% result in citation numbers being automatically sorted and properly
% "compressed/ranged". e.g., [1], [9], [2], [7], [5], [6] without using
% cite.sty will become [1], [2], [5]--[7], [9] using cite.sty. cite.sty's
% \cite will automatically add leading space, if needed. Use cite.sty's
% noadjust option (cite.sty V3.8 and later) if you want to turn this off
% such as if a citation ever needs to be enclosed in parenthesis.
% cite.sty is already installed on most LaTeX systems. Be sure and use
% version 5.0 (2009-03-20) and later if using hyperref.sty.
% The latest version can be obtained at:
% http://www.ctan.org/pkg/cite
% The documentation is contained in the cite.sty file itself.
%
% Note that some packages require special options to format as the Computer
% Society requires. In particular, Computer Society papers do not use
% compressed citation ranges as is done in typical IEEE papers
% (e.g., [1]-[4]). Instead, they list every citation separately in order
% (e.g., [1], [2], [3], [4]). To get the latter we need to load the cite
% package with the nocompress option which is supported by cite.sty v4.0
% and later.
% *** GRAPHICS RELATED PACKAGES ***
%
\ifCLASSINFOpdf
% \usepackage[pdftex]{graphicx}
% declare the path(s) where your graphic files are
% \graphicspath{{../pdf/}{../jpeg/}}
% and their extensions so you won't have to specify these with
% every instance of \includegraphics
% \DeclareGraphicsExtensions{.pdf,.jpeg,.png}
\else
% or other class option (dvipsone, dvipdf, if not using dvips). graphicx
% will default to the driver specified in the system graphics.cfg if no
% driver is specified.
% \usepackage[dvips]{graphicx}
% declare the path(s) where your graphic files are
% \graphicspath{{../eps/}}
% and their extensions so you won't have to specify these with
% every instance of \includegraphics
% \DeclareGraphicsExtensions{.eps}
\fi
% graphicx was written by David Carlisle and Sebastian Rahtz. It is
% required if you want graphics, photos, etc. graphicx.sty is already
% installed on most LaTeX systems. The latest version and documentation
% can be obtained at:
% http://www.ctan.org/pkg/graphicx
% Another good source of documentation is "Using Imported Graphics in
% LaTeX2e" by Keith Reckdahl which can be found at:
% http://www.ctan.org/pkg/epslatex
%
% latex, and pdflatex in dvi mode, support graphics in encapsulated
% postscript (.eps) format. pdflatex in pdf mode supports graphics
% in .pdf, .jpeg, .png and .mps (metapost) formats. Users should ensure
% that all non-photo figures use a vector format (.eps, .pdf, .mps) and
% not a bitmapped formats (.jpeg, .png). The IEEE frowns on bitmapped formats
% which can result in "jaggedy"/blurry rendering of lines and letters as
% well as large increases in file sizes.
%
% You can find documentation about the pdfTeX application at:
% http://www.tug.org/applications/pdftex
% *** MATH PACKAGES ***
%
%\usepackage{amsmath}
% A popular package from the American Mathematical Society that provides
% many useful and powerful commands for dealing with mathematics.
%
% Note that the amsmath package sets \interdisplaylinepenalty to 10000
% thus preventing page breaks from occurring within multiline equations. Use:
%\interdisplaylinepenalty=2500
% after loading amsmath to restore such page breaks as IEEEtran.cls normally
% does. amsmath.sty is already installed on most LaTeX systems. The latest
% version and documentation can be obtained at:
% http://www.ctan.org/pkg/amsmath
% *** SPECIALIZED LIST PACKAGES ***
%
%\usepackage{algorithmic}
% algorithmic.sty was written by Peter Williams and Rogerio Brito.
% This package provides an algorithmic environment fo describing algorithms.
% You can use the algorithmic environment in-text or within a figure
% environment to provide for a floating algorithm. Do NOT use the algorithm
% floating environment provided by algorithm.sty (by the same authors) or
% algorithm2e.sty (by Christophe Fiorio) as the IEEE does not use dedicated
% algorithm float types and packages that provide these will not provide
% correct IEEE style captions. The latest version and documentation of
% algorithmic.sty can be obtained at:
% http://www.ctan.org/pkg/algorithms
% Also of interest may be the (relatively newer and more customizable)
% algorithmicx.sty package by Szasz Janos:
% http://www.ctan.org/pkg/algorithmicx
% *** ALIGNMENT PACKAGES ***
%
%\usepackage{array}
% Frank Mittelbach's and David Carlisle's array.sty patches and improves
% the standard LaTeX2e array and tabular environments to provide better
% appearance and additional user controls. As the default LaTeX2e table
% generation code is lacking to the point of almost being broken with
% respect to the quality of the end results, all users are strongly
% advised to use an enhanced (at the very least that provided by array.sty)
% set of table tools. array.sty is already installed on most systems. The
% latest version and documentation can be obtained at:
% http://www.ctan.org/pkg/array
% IEEEtran contains the IEEEeqnarray family of commands that can be used to
% generate multiline equations as well as matrices, tables, etc., of high
% quality.
% *** SUBFIGURE PACKAGES ***
%\ifCLASSOPTIONcompsoc
% \usepackage[caption=false,font=footnotesize,labelfont=sf,textfont=sf]{subfig}
%\else
% \usepackage[caption=false,font=footnotesize]{subfig}
%\fi
% subfig.sty, written by Steven Douglas Cochran, is the modern replacement
% for subfigure.sty, the latter of which is no longer maintained and is
% incompatible with some LaTeX packages including fixltx2e. However,
% subfig.sty requires and automatically loads Axel Sommerfeldt's caption.sty
% which will override IEEEtran.cls' handling of captions and this will result
% in non-IEEE style figure/table captions. To prevent this problem, be sure
% and invoke subfig.sty's "caption=false" package option (available since
% subfig.sty version 1.3, 2005/06/28) as this is will preserve IEEEtran.cls
% handling of captions.
% Note that the Computer Society format requires a sans serif font rather
% than the serif font used in traditional IEEE formatting and thus the need
% to invoke different subfig.sty package options depending on whether
% compsoc mode has been enabled.
%
% The latest version and documentation of subfig.sty can be obtained at:
% http://www.ctan.org/pkg/subfig
% *** FLOAT PACKAGES ***
%
%\usepackage{fixltx2e}
% fixltx2e, the successor to the earlier fix2col.sty, was written by
% Frank Mittelbach and David Carlisle. This package corrects a few problems
% in the LaTeX2e kernel, the most notable of which is that in current
% LaTeX2e releases, the ordering of single and double column floats is not
% guaranteed to be preserved. Thus, an unpatched LaTeX2e can allow a
% single column figure to be placed prior to an earlier double column
% figure.
% Be aware that LaTeX2e kernels dated 2015 and later have fixltx2e.sty's
% corrections already built into the system in which case a warning will
% be issued if an attempt is made to load fixltx2e.sty as it is no longer
% needed.
% The latest version and documentation can be found at:
% http://www.ctan.org/pkg/fixltx2e
%\usepackage{stfloats}
% stfloats.sty was written by Sigitas Tolusis. This package gives LaTeX2e
% the ability to do double column floats at the bottom of the page as well
% as the top. (e.g., "\begin{figure*}[!b]" is not normally possible in
% LaTeX2e). It also provides a command:
%\fnbelowfloat
% to enable the placement of footnotes below bottom floats (the standard
% LaTeX2e kernel puts them above bottom floats). This is an invasive package
% which rewrites many portions of the LaTeX2e float routines. It may not work
% with other packages that modify the LaTeX2e float routines. The latest
% version and documentation can be obtained at:
% http://www.ctan.org/pkg/stfloats
% Do not use the stfloats baselinefloat ability as the IEEE does not allow
% \baselineskip to stretch. Authors submitting work to the IEEE should note
% that the IEEE rarely uses double column equations and that authors should try
% to avoid such use. Do not be tempted to use the cuted.sty or midfloat.sty
% packages (also by Sigitas Tolusis) as the IEEE does not format its papers in
% such ways.
% Do not attempt to use stfloats with fixltx2e as they are incompatible.
% Instead, use Morten Hogholm'a dblfloatfix which combines the features
% of both fixltx2e and stfloats:
%
% \usepackage{dblfloatfix}
% The latest version can be found at:
% http://www.ctan.org/pkg/dblfloatfix
% *** PDF, URL AND HYPERLINK PACKAGES ***
%
\usepackage{url}
% url.sty was written by Donald Arseneau. It provides better support for
% handling and breaking URLs. url.sty is already installed on most LaTeX
% systems. The latest version and documentation can be obtained at:
% http://www.ctan.org/pkg/url
% Basically, \url{my_url_here}.
% *** Do not adjust lengths that control margins, column widths, etc. ***
% *** Do not use packages that alter fonts (such as pslatex). ***
% There should be no need to do such things with IEEEtran.cls V1.6 and later.
% (Unless specifically asked to do so by the journal or conference you plan
% to submit to, of course. )
\usepackage{tikz}
\usepackage{amsmath}
\usepackage{xcolor}
\usepackage{subcaption}
\usepackage{listings}
\usepackage{framed}
\usepackage{fancyhdr}
\usepackage{tabularx}
\usepackage{adjustbox}
\usepackage[normalem]{ulem}
\usepackage{graphicx}
\usepackage{booktabs}
\usepackage{enumitem}
\usepackage[plainpages=false]{hyperref}
%\usepackage{caption}
%\captionsetup[table]{skip=10pt}
\lstdefinestyle{verilog-style}
{
language=Verilog,
basicstyle=\small\ttfamily,
keywordstyle=\color{black},
identifierstyle=\color{black},
commentstyle=\color{black},
numbers=left,
basicstyle=\small,
numberstyle=\tiny\color{black},
numbersep=10pt,
tabsize=8,
%moredelim=*[s][\colorIndex]{[}{]},
literate=*{:}{:}1
}
\newcommand{\cks}[1]{\textcolor{blue}{cks: #1}}
\newcommand{\kar}[1]{\textcolor{red}{kar: #1}}
\newcommand{\mg}[1]{\textcolor{green}{mg: #1}}
% correct bad hyphenation here
\hyphenation{op-tical net-works semi-conduc-tor}
\hypersetup{ colorlinks = true, %Colours links instead of ugly boxes
urlcolor = blue, %Colour for external hyperlinks
linkcolor = blue, %Colour of internal links
citecolor = blue %Colour of citations
}
\begin{document}
%
% paper title
% Titles are generally capitalized except for words such as a, an, and, as,
% at, but, by, for, in, nor, of, on, or, the, to and up, which are usually
% not capitalized unless they are the first or last word of the title.
% Linebreaks \\ can be used within to get better formatting as desired.
% Do not put math or special symbols in the title.
\title{Augmented Symbolic Execution for Information Flow in Hardware
Designs}
% author names and affiliations
% use a multiple column layout for up to three different
% affiliations
\author{\IEEEauthorblockN{Anon}}
%% \IEEEauthorblockA{School of Electrical and\\Computer Engineering\\
%% Georgia Institute of Technology\\
%% Atlanta, Georgia 30332--0250\\
%% Email: http://www.michaelshell.org/contact.html}
%% \and
%% \IEEEauthorblockN{Homer Simpson}
%% \IEEEauthorblockA{Twentieth Century Fox\\
%% Springfield, USA\\
%% Email: homer@thesimpsons.com}
%% \and
%% \IEEEauthorblockN{James Kirk\\ and Montgomery Scott}
%% \IEEEauthorblockA{Starfleet Academy\\
%% San Francisco, California 96678-2391\\
%% Telephone: (800) 555--1212\\
%% Fax: (888) 555--1212}}
% conference papers do not typically use \thanks and this command
% is locked out in conference mode. If really needed, such as for
% the acknowledgment of grants, issue a \IEEEoverridecommandlockouts
% after \documentclass
% for over three affiliations, or if they all won't fit within the width
% of the page (and note that there is less available width in this regard for
% compsoc conferences compared to traditional conferences), use this
% alternative format:
%
\author{\IEEEauthorblockN{Kaki Ryan}
University of North Carolina \\
Chapel Hill, NC, USA
\and
\IEEEauthorblockN{Matthew Gregoire}
University of North Carolina \\
Chapel Hill, NC, USA
\and
\IEEEauthorblockN{Cynthia Sturton}
University of North Carolina \\
Chapel Hill, NC, USA
}
% use for special paper notices
%\IEEEspecialpapernotice{(Invited Paper)}
% make the title area
\maketitle
% As a general rule, do not put math, special symbols or citations
% in the abstract
\begin{abstract}
We present \emph{SEIF}, a methodology that combines static analysis with
symbolic execution to verify and explicate information flow paths in a hardware
design. SEIF begins with a statically built model of the information flow through a
design and uses guided symbolic execution to recognize and eliminate
non-flows with high precision or to find corresponding paths through the design
state for true flows. We evaluate SEIF on two open-source CPUs, an AES core, and the
AKER access control module. SEIF can exhaustively explore 10-12 clock cycles deep in
4-6 seconds on average, and can automatically account for 86-90\% of
the paths in the statically built model. %% , verifying 58-77\% of them as repayable from the design's
%% reset state.
Additionally, SEIF can be used to find multiple violating paths for security
properties, providing a new angle for security verification.
%10 pages, excluding refs and appdx
\end{abstract}
% no keywords
% For peer review papers, you can put extra information on the cover
% page as needed:
% \ifCLASSOPTIONpeerreview
% \begin{center} \bfseries EDICS Category: 3-BBND \end{center}
% \fi
%
% For peerreview papers, this IEEEtran command inserts a page break and
% creates the second title. It will be ignored for other modes.
\IEEEpeerreviewmaketitle
\input{introduction}
\input{threatmodel}
\input{preliminaries}
\input{design}
\input{implementation}
\input{evaluation}
\input{related}
\input{conclusion}
\input{acknowledgments}
\input{references}
%% % use section* for acknowledgment
%% \ifCLASSOPTIONcompsoc
%% % The Computer Society usually uses the plural form
%% \section*{Acknowledgments}
%% \else
%% % regular IEEE prefers the singular form
%% \section*{Acknowledgment}
%% \fi
%% The authors would like to thank...
% trigger a \newpage just before the given reference
% number - used to balance the columns on the last page
% adjust value as needed - may need to be readjusted if
% the document is modified later
%\IEEEtriggeratref{8}
% The "triggered" command can be changed if desired:
%\IEEEtriggercmd{\enlargethispage{-5in}}
% references section
% can use a bibliography generated by BibTeX as a .bbl file
% BibTeX documentation can be easily obtained at:
% http://mirror.ctan.org/biblio/bibtex/contrib/doc/
% The IEEEtran BibTeX style support page is at:
% http://www.michaelshell.org/tex/ieeetran/bibtex/
%\bibliographystyle{IEEEtran}
% argument is your BibTeX string definitions and bibliography database(s)
%\bibliography{IEEEabrv,../bib/paper}
%\bibliography{references}
%
% <OR> manually copy in the resultant .bbl file
% set second argument of \begin to the number of references
% (used to reserve space for the reference number labels box)
%% \begin{thebibliography}{1}
%% \bibitem{IEEEhowto:kopka}
%% H.~Kopka and P.~W. Daly, \emph{A Guide to \LaTeX}, 3rd~ed.\hskip 1em plus
%% 0.5em minus 0.4em\relax Harlow, England: Addison-Wesley, 1999.
%% \end{thebibliography}
\include{appendix}
% that's all folks
\end{document}
\section{Introduction}
%% This paper presents \textit{SEIF} (pronounced ``safe''), a toolflow that combines static analysis with symbolic execution
%% for verifying information flow paths in hardware designs. SEIF begins with a static model of the information flows
%% through a design and is able to produce realizable and semantically accurate information flow paths. This is made
%% possible by an augmented symbolic execution engine with heuristics that steer the search towards paths
%% necessary to complete the flow. The search space would otherwise be intractable.
%% SEIF is able to produce counterexamples when given a security property, in addition
%% to providing all of the replayable information flow paths that exhibit the vulnerable behavior.
%% Analyzing information flow is important for security
Analyzing how information flows through a hardware design is critical
to verifying the security of the design~\cite{tiwari2009complete,tiwari2009execution,jin2012proof,li2011caisson,li2014sapper,zhang2015secverilog, bidmeshki2015vericoq, hu2016detecting,kong2017using,ardeshiricham2017register,ardeshiricham2017clepsydra,deng2017secchisel,bidmeshki2017information,boraten2018securing,pilato2018tainthls,zagieboylo2019using,pieper2020dynamic}.
Unwanted flows of information to
or from a signal in the design can violate desired security policies in the form of
access authorization
violations~\cite{restuccia2021aker,restuccia2022framework}, memory leakage
vulnerabilities~\cite{cherupalli2017software,fadiheh2023exhaustive}, %% \cks{smthg for Isadora
%% paper~\cite{Deutschbein2021Isadora,Deutschbein2022JCEN}, Chapter in
%% txtbk~\cite{sturton2022handbook}, Kastner's survey paper on IF Verification~\cite{??}},
and possible privilege escalation vulnerabilities~\cite{wu2022exert}.
Recent work has shown that symbolic execution
is a powerful tool for analyzing how information flows through a hardware
design~\cite{athalye2022knox,fowze2022eisec,cherupalli2017software}. Symbolic analysis is
precise and enables
tracking both direct and indirect flows of information through each path of
execution without instrumenting the design with added tracking logic.
%% Current practice for detecting and
%% understanding these flows uses simulation-based testing~\cite{smth}, static
%% analysis~\cite{smth}, or most recently, symbolic execution~\cite{smth}.
%% Still not a solved problem
Unfortunately, symbolic execution infamously suffers from the path explosion
problem. The number of paths through a design grows exponentially with the
number of branch points in the design. Hardware designs have the added
complexity of reasoning about paths over multiple clock cycles in order to
realize complete flows of information from an input port (source) signal to an output
port (sink) signal. Current solutions to the path explosion problem have been to consider
small, but security critical designs~\cite{athalye2022knox,fowze2022eisec}, or to constrain the hardware design
space by analyzing how information flows for a particular software program~\cite{cherupalli2017software,athalye2019notary}.
%% Static analysis plus symbolic execution is the answer!
We take a different approach. We start with static analysis, using an existing
tool~\cite{meza2023hyperflowgraph} to
build a graph that over-approximates how information flows
through a design. Such a graph is useful for designers, allowing them to explore
their design and find possible illegal or insecure flows. %% We show that
%% by using the information in this graph to guide the symbolic execution engine, we
%% can fully explore how information flows from an input port signal of interest through
%% a design for a sufficient number of clock cycles for the flow to reach all possible
%% output ports. The approach can scale to full CPU designs. (In our experiments this is typically \cks{XX-XX} clock cycles for
%% an open-source CPU~\ref{evaluation}.)
For our purposes, the graph provides useful information that can be used to guide
symbolic execution: a sequence of landmark points in
the hardware design that execution must reach in order to
realize a given path of information flow. Using these landmarks as a guide, we use symbolic
execution to improve the graph's efficacy: finding a realizable path through the
design state, along with the inputs needed to take that path, corresponding to a
path in the graph; recognizing and eliminating from the graph paths which are
unrealizable in execution; and recognizing and eliminating from the graph paths
which are realizable, but do not represent a true flow of information.
%% some paths as unrealizable, and for the paths remaining, develop
%% heuristics that steer
%% symbolic execution toward paths more likely to result in the desired information flow.
%% But the graph does not tell us which paths
%% of execution to take in order to get to each subsequent in landmark when we are looking
%% at a path made up of a sequence of many information flows. It also doesn't tell us
%% how long (how many clock cycles of execution) it will take to get there, or whether it is even
%% possible to get to the next landmark at all from current one. To answer these
%% questions we use develop and implement search heuristics based on SMT solving into a symbolic execution
%% engine. \cks{This is a
%% reachability problem. Piecewise reachability? Stepwise reachability?}
%% %stalling, unsat core?, backtracking.
This paper presents \textit{SEIF} (pronounced ``safe''), a toolflow that
combines symbolic execution with static analysis in the form of the information
flow graph. SEIF takes as input the statically built
information flow (IF) graph and the source signals of interest in the design.
Three
outcomes are possible: 1. SEIF finds that the path is unrealizable or does not
represent a true flow of information, and requires no
further scrutiny from the security engineer, 2. SEIF returns a sequence of input
values that will drive the design along the IF-graph path to realize the flow of
information, or 3. the complexity of the search space
leaves the IF-graph path unaccounted for.
To find that a path is unrealizable or does not represent a true flow of
information, SEIF uses two mechanisms: a check for mutually contradictory constraints and symbolic
analysis. If the first mechanism reports that a path is unrealizable then it is, regardless of the
number of clock cycles the design is allowed to run. If the second mechanism
reports that a path is unrealizable, then it is within the clock cycle bound used
by SEIF. In our experiments, this was the case for 5-7\% of the paths.
To find and return a sequence of input values that will drive execution along an
IF-graph path, SEIF uses symbolic execution guided by the IF graph and
heuristics we develop. The returned
sequence of input values will drive execution along the IF-graph path, either
starting from the design's reset state or from an intermediate state. In our
evaluation (Section~\ref{sec:eval}) we differentiate these two cases.
%% However, as is always the
%% theoretical limit, this analysis cannot be both sound and complete. The analysis
%% is bounded in the number of clock cycles explored and may report that a path was
%% not found within the given bound.
%% % start talking about how our methodology is exploratory / not property -based
%% Current practice in hardware security verification is property
%% driven~\cite{hu2016towards}, which requires a security engineer to develop a set
%% of properties for use with the verification engine. This often involves manual
%% review of the design and of CWEs, and can yield many properties for a relatively small design~\cite{restuccia2022framework}.
%% A new trend in hardware security is to build a map of the design that supports the designer in their understanding
%% of security-critical information flows~\cite{Deutschbein2021Isadora,Deutschbein2022JCEN}.
%% Our methodology is in keeping with this new trend and allows users
%% to perform more exploratory analyses.
%% \cks{I'm commenting out for now, but it could go in the eval section potentially}
%% \kar{rough}
%% When verifying a specific security property, a commercial tool like JasperGold SPV will provide a single counterexample.
%% It takes a large amount of manual effort to generate subsequent counterexamples using a bit-level formal tool like JasperGold SPV
%% because it involves asserting additional preconditions and constraints over your property.
%% Our approach can provide the user with all of the candidate violating flow paths automatically.
%% Once we find a security-critical flow, we can continue exploring further by identifying the sinks reachable from that source.
%% This could potentially uncover things not specified in the original property (if there was one)
%\cks{From conversation with Kaki:} Symbolic execution is inherently a tool for
%security validation (of hardware designs) -- cite a bunch of examples -- and we
%can do it at scale (for this one particular problem of finding information flow
%paths. this is a type of reachability analysis?) -- evaluation must show that we
%can scale in ways that prior work could not and for security problems that are
%of interest to the community (e.g., b/c they show up in prior security testing,
%model checking, SE work) Can we tackle larger designs than prior SE work could?
%Can we find paths that other approaches (e.g., testing-based, tortuga, cadence)
%could not?
%and use symbolic
%execution to eliminate false positives, provide concrete testbenches for the
%paths that remain, and provide metrics of the elasticity/malleability of the
%remaining paths, which can be helpful when determining how dangerous a path may
%be in practice and prioritizing patches. We introduce new techniques based on SMT
%solving to recognize and eliminate
%impossible paths of flow early, and we develop heuristics to guide the search
%toward paths more likely to exhibit the searched-for flows. With these
%techniques, and using the results from static analysis as a guide, the
%approach can scale to full SoCs/NoCs.
%% The gist of our approach
%% Use static analysis to build a possible path of information flow. Divide each
%% path into clock cycle boundaries. Use symbolic execution to explore the design
%% to find a 1-clock-cycle path matching the path fragment. Unsat core evaluation
%% guides the search and eliminates impossible paths quickly.
%% The contribution
In this paper, we develop SEIF, an algorithm and tool to search for and eliminate
false paths of information flow from a static analysis of a hardware
design and then to further explicate the paths that remain. We show that by
using the static analysis as a guide, we can guide symbolic execution toward more probable paths and eliminate impossible paths
early. Our contributions are:
\begin{itemize}
\item Define \emph{SEIF}, an augmented symbolic execution methodology for information flow
analysis. %% Develop the use of symbolic execution with unsat core
%% evaluation to efficiently remove false positive paths from a static information
%% flow analysis and enable more dynamic security analysis
\item Implement the methodology and search heuristics on top of the symbolic execution engine discussed in \cite{ryan2023countering}.
\item Evaluate the augmented symbolic execution strategy on four open-source designs.
\end{itemize}
%\cks{Some possible additional ways to frame work}
%1. Tools like Cadence SPV work one path at a time. We can help understand how many
%paths exist. We also can provide timing/clock-cycle information that could be
%useful for patches/mitigations to make sure the patch isn't introducing race
%conditions. It may also be helpful in developing patches to be able to say this
%is the minimum number of clock cycles an IF-path can take and this
%is the earliest clock cycle in which a segment of the IF path can occur.
%2. As a metric to help understand how dangerous an undesirable path is. If there
%exist many paths through the design that realize the same IF-path, this is a
%more dangerous IF-path b/c the attacker is less constrained in coming up with
%the relevant inputs.
%3. If the design can stall (stutter w/r.t. the IF-path) this is more dangerous
%b/c it is easier to provide attack inputs that realize the IF-path. The attacker
%can still launch a successful attack even if they cannot control the input on
%every clock cycle. This is slightly different than the analysis we do in our
%search strategy when determining if the search *must* stall. Essentially, These
%metrics are a measure of the ``window of attack'' available to the attacker. It
%could be good to evaluate these on the OpenTitan design b/c Andy found that all
%IF-paths found in the OTP-to-AES core they analyzed were realizable. I.e., we
%won't find any false positives.
%\kar{My notes with ideas about framing/eval}
%1.If we have more paths realizing the same iflow path, this could potentially indicate the flow
%is more dangerous. Right now Sylvia stops when it finds the first path realizing a flow,
%but in the eval this is one number we might want to show -- how many Sylvia paths realize the same iflow path.
% 2. Timing. Design can run for many cycles without impacting flow (information staying in registers)
% This information can be exploited later.. this is potentially more dangerous, too. Look at this in eval.
% Idea of "window of attack" / ease of attack mitigation (I dont think I remember what the second is)
% 3. potentially producing heatmap/visualization of realizable paths.. we can produce observations that
% many flows may be going into one sink/signal --> do we trust this thing? are we ok with this? would give
% us groups of signals for further analysis/to look into
% 4. our tool gives multiple paths (potentially) which is helpful for the designer whereas a tool like SPV just gives one,
% can find others using SMT, but this is tedious and takes longer
% We can describe our tool as providing security-related metrics.
% Andy leaves the FP in the graph, but used test benches and manually weed them out/identify later --> this is is another angle where we come in,
% getting rid of this manual process.
%% \url{https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=9155136}~\cite{micinski2020abstracting}. Static analysis of SW using abstract interpretation for information flow analysis.
%% static analysis of information flow in SW, used to make dynamic information flow
%% analysis more efficient by removing unnecessary runtime checks. Too
%% tangential to this work.
%% \cks{from NSF proposal:}
%% Determining how information flows through the design is fundamental to understanding the hardware's security~\cite{tiwari2009complete, tiwari2009execution, jin2012proof, ferraiuolo2017verification, li2011caisson, li2014sapper, zhang2015secverilog, bidmeshki2015vericoq, hu2016detecting, kong2017using, ardeshiricham2017register, ardeshiricham2017clepsydra, deng2017secchisel, bidmeshki2017information, boraten2018securing, pilato2018tainthls, zagieboylo2019using, pieper2020dynamic}.
\section{Threat Model}
Information-flow analysis is a part of the security validation
activities~\cite{dorsey2020intel} that take place during the design phase of
the hardware lifecycle~\cite{he2015model}. The goal is to find
weaknesses, vulnerabilities, and flaws in register transfer level (RTL)
designs that may be exploitable post-deployment.
%% Our threat model is an attacker, or colluding attackers, acting in the
%% post-deployment phase, after the hardware has been fabricated and shipped. The
%% attackers aim to exploit a hardware vulnerability to gain unauthorized access to
%% data or execution. For example, a hardware flaw may allow the attacker to learn
%% confidential data stored in memory or hardcoded into a device, or it may allow
%% the attacker to modify the control flow of software running on a processor by
%% leveraging aspects of the processor's behavior. The attacker may access the
%% hardware locally. Remote attacks caused by running attacker-controlled software
%% (e.g., JavaScript on a website visited by the machine) are feasible. Physical
%% attacks, including hardware tampering, fault injection, and power or
%% electromagnetic side channels, are out of scope.
Flaws that result from logic and physical synthesis
tools, manufacturing, or the supply chain cannot be discovered by SEIF.
We target flaws that occur by benign human error in the specification,
design, or implementation phases. Our analysis may find maliciously
inserted flaws, they will have a lower chance of being uncovered than benign
flaws as the attacker will likely take steps to hide their work,
so that the security engineer does not recognize the
malicious flow of information as dangerous. Flaws maliciously inserted after the
security validation is complete, e.g., analog Trojans~\cite{YangSP2016}, cannot
be discovered by SEIF.
%% Finally, the security engineer who is conducting the information-flow analysis
%% is trusted to act in good faith. The goal of our tool is to help the engineer
%% pare down the set of possible flows of information requiring study, and provide
%% concrete test cases for true flows of information to help the engineer better
%% understand the design. This tool supports the imperfect engineer by helping them
%% to understand the design better and highlight the security implications of
%% various information flows.
\section{Problem Statement}
We approach the problem of information-flow analysis by
transforming it into a graph reachability problem over a labeled, directed graph
representing signal connectivity, extracted from the Verilog RTL design. We use symbolic execution of the RTL
to determine which paths through the labeled directed graph represent true flows of information through
the design in execution.
%We can also think of this as using symbolic execution to model how
%information flows through the design, and using the static signal connectivity graph
%to guide the symbolic execution engine through the
%large search space.
%The signal connectivity graph helps us tackle
%the path explosion problem inherent in symbolic execution.
%Our problem statement is as follows.
%Given a hardware design at the register transfer level (RTL), and an input
%signal of interest, $x$, determine the information
%flow of that signal. Information flows from signal $x$ to signal $y$ when the value
%of $y$ at any clock cycle depends on or is influenced by the value of $x$.
%This
%definition allows for checking
%non-interference~\cite{goguen1982security}: under this definition, we can say
%that $x$ is non-interfering with
% $y$ if there exist no execution traces
%in which $x$ flows to $y$.
Given a hardware design and a particular input signal of
interest, the goal is to return:
\begin{enumerate}[noitemsep]
\item the set of realizable information flows through the design originating at
that signal; and
\item for each found information flow, return a sequence of input values to the design that will
drive the information flow.
%% \item \cks{OR: (Kaki, which do you think is more accurate?)}
%% \item the set of variables in the design that are influenced by the input
%% signal $v$; and
%% \item for each found signal, return a sequence of input values to the design
%% that will drive the information flow from $v$ to that signal.
\end{enumerate}
\section{Preliminaries}
It is useful to keep in
mind three models: the state diagram of the design
showing machine states and transitions between them; the labeled, directed, signal-connectivity graph, which we
call the \emph{Information Flow (IF)} graph; and the symbolic execution
(SE) tree, showing execution paths through the RTL along with the associated
(symbolic) states and path conditions. We describe these three in the following
sections, but first we introduce a fragment of Verilog RTL as a toy example to
help illustrate the three models.
\subsection{Toy Example}
The code snippet of Figure~\ref{fig:toy1} shows a flow from an input, \texttt{secret}, to an output, \texttt{led}. The flow is
guarded by an internal, state-holding variable and the secret will only flow to the
LED output in the clock cycle after $\mathtt{state} = 3$. Note that with non-blocking assignments (``$<=$'')
all right-hand side expressions are calculated at the same time and assignments
take effect at the next clock cycle. Blocking assignments (``$=$'') take effect
immediately.
\begin{figure}[h!]
\centering
\begin{framed}
\begin{lstlisting}[style={verilog-style},belowskip=-.8\baselineskip,aboveskip=-.5\baselineskip]
always @(posedge clk) begin
if (enable) begin
prev <= state;
state <= state + 1;
end
if (state == 3) begin
guard <= secret;
end else begin
guard <= 0;
end
end
assign led = (prev == 3) ? guard : 0;
\end{lstlisting}
\end{framed}
\caption{Toy example. \texttt{clk}, \texttt{enable}, and \texttt{secret} are input \textbf{wire}s.
\texttt{state}, \texttt{prev}, and \texttt{guard} are state-holding \textbf{reg}s. Not
shown is the initialization, which sets \texttt{state}, \texttt{prev}, and \texttt{guard} to 0.
\texttt{led} is an output wire. \texttt{secret} flows through \texttt{guard} to
\texttt{led} after four clock cycles.}
\label{fig:toy1}
\end{figure}
\subsection{State Diagram}
We model a
hardware design as a tuple, $D = (S, s_0, I, \delta, \omega)$,
where
\begin{itemize}[noitemsep]
\item $S$ is the set of states of the design;
\item $S_0 \subset S$ is the set of initial states;
\item $I$ is the finite set of input strings;
\item $\delta: S \times I \rightarrow S$ is the transition function;
\item $\omega: S \rightarrow O$ is the output function.
\end{itemize}
A state $s \in S$ is a vector of valuations to state-holding internal variables of the design,
$s = \langle v_0, v_1, \ldots, v_{|s|}\rangle$. We use $v_i$
to indicate the variable and $\langle v_i = x \rangle_{s_j}$ to indicate that the value of
variable $v_i$ is $x$ in state $s_j$. As shorthand, we sometimes use $v_i$ to
refer to both the variable and its value, when it is clear in the text what we
mean. The design powers up in an
initial state, $s_0$. Many state-holding variables are reset to 0 in the initial
state. An input string $i \in I$ is a concatenation of values to input variables
of the design. Inputs are provided on every clock cycle. Similarly to
state-holding variables, we refer to the value of input variable $v_j$ at any given clock
cycle as $\langle v_j = x \rangle$ or simply $v_j$. The
\texttt{clk} signal is a special input that synchronizes reading input values and state
transitions, which happen on clock cycle edges. The output function is the
identity function over a subset of the design's variables.
For example, Figure~\ref{fig:toy1states} shows a sequence of state transitions for the toy example, starting
with the initial state, in which
information flows from
\texttt{secret} to \texttt{guard} to output variable \texttt{led}.
In this example, the initial state $s_0 = \langle
\texttt{prev} = 0, \texttt{state} = 0, \texttt{guard} = 0\rangle$ produces output
$\omega(s_0) = \langle\texttt{led} = 0\rangle$, and transitions to state $s_1 = \langle\texttt{prev} = 0,
\texttt{state} = 1, \texttt{guard} = 0\rangle$ when \texttt{enable} is high on a positive clock edge.
\begin{figure}[h]
\centering
\setlength{\belowcaptionskip}{-10pt}
\includegraphics[width=\columnwidth,trim = 15 225 30 125, clip]{figures/toy1states}
\caption{State transitions of the toy example (Figure~\ref{fig:toy1}) in which information flows from
\texttt{secret} to \texttt{led}.}
\label{fig:toy1states}
\end{figure}
\subsection{Information Flow (IF) Graph}
The Information Flow (IF) graph is a labeled, directed graph that captures signal
connectivity and provides additional information, taken from the Verilog source,
about the conditions under which two signals are connected~\cite{meza2023hyperflowgraph}. Nodes represent the variables (\texttt{wire}s
and \texttt{reg}s) of the design, and edges indicate a possible flow of
information from one variable to another. An edge $(v_1,v_2)$
exists when either there is an assignment from $v_1$ to $v_2$ (e.g., $v_2 <=
v_1$) or $v_1$ appears in a condition (e.g., $\mathtt{if} (v_1)$), and $v_2$ appears
on the left-hand side of an assignment in either branch. The edge is labeled
with the line number of the relevant Verilog statement and lists the surrounding
conditions in the code that must be true for the information flow to take
place. For example, in Figure~\ref{fig:toy1ifg}, which shows the IF graph for the code in
Figure~\ref{fig:toy1}, the edge $(\mathtt{secret}, \mathtt{guard})$ would be
labeled with the condition that $\mathtt{state} == 3$. Note that this graph inherently has no notion of timing or
clock cycles.
\begin{figure}[h]
\centering
\setlength{\belowcaptionskip}{-5pt}
\includegraphics[scale=0.20]{figures/toy1ifg}
\caption{An IF graph for the code in Figure~\ref{fig:toy1}. Dashed lines represent implicit flows
of information and solid lines represent explicit flows. Labels are
omitted for space.}
\label{fig:toy1ifg}
\end{figure}
Each edge in the IF graph represents a viable 1-hop flow of
information in the design. However, multi-hop paths through the IF graph may not
correspond to viable information flows. In other words, if
we view the IF graph as an information-flow relation, taking the
transitive closure of the relation yields an over-approximation of information
flow through the design. To demonstrate, consider the code in
Figure~\ref{fig:toy1}, but with the last line replaced with the following:
\begin{verbatim}
assign led = (prev == 2) ? guard : 0;
\end{verbatim}
The IF graph would have the same nodes and edges, but the path from
\texttt{secret} to \texttt{guard} to \texttt{led} does not correspond to any
flow of information through the design.
There are two reasons why a path through the IF graph may not correspond to a
true information flow. The first is that, as in the example above,
the sequence of conditions needed for
each edge cannot be satisfied. The second is that a path through the IF graph
from $x$ to $y$ may not correspond to a true flow of
information in the sense that the value of $y$ depends on the value of $x$. A
common example of this is the assignment $y = x \oplus x$.
%We use symbolic execution to find which
%paths through the IF graph represent true flows of information through the design.
\subsection{Symbolic Execution}
In symbolic execution, concrete input values are replaced with abstract
symbols. The design is executed using the symbols in place of
literals. When a branch point (e.g., $\mathtt{if}$\texttt{(enable)}) is reached, both paths are separately
explored. For each path, the branching condition that must be true for that path
(e.g., \texttt{enable} $== 1$).
is maintained in the
\emph{path condition}. At the end of a single path of symbolic execution, satisfying
assignments to the constraints in the path condition can be used as concrete
input values to drive concrete execution down that same path.
Symbolic execution is modeled as a directed tree. Each node $n$ in the tree
is associated with a line of code in the design and is associated with a symbolic state, $\sigma$, and path condition, $\pi$. A node's children are the possible next
lines of code to symbolically execute. A path from the root node to any leaf
node represents a realizable path through the design.
The number of paths to explore grows quickly. For example, the symbolic execution of the design in Figure~\ref{fig:toy1} for
the four clock cycles necessary to find the information-flow path from
\texttt{secret} to \texttt{led} would yield the tree of nodes shown in Figure~\ref{fig:toy1tree}.
%%
%%
%% single clock cycle, starting from the initial state and initializing inputs
%% \texttt{enable} and \texttt{secret} with symbolic values $\alpha$, and $\beta$,
%% respectively, would yield two leaf nodes: $n_1 = (\sigma
%%
%% , one in which \texttt{enable} is high
%% and one in which it is low. a tree with 8 leaf nodes corresponding to 8 paths
%% through the design. Let \texttt{enable} and \texttt{secret} be initialized with
%% symbolic values $\alpha$ and $\beta$. Following the one-clock-cycle path from
%% the initial state in which \texttt{enable} is high would end
%%
%% the 4-clock cycle path in Figure~\ref{fig:toy1tree} in which information flows
%% from \texttt{secret} to \texttt{led} has path constraint $\pi = ()$ and ends in symbolic
%% state $\sigma = ()$.
%\cks{Kaki, please Double check that I'm not
%off by one.}
A single path through the IF graph can correspond to many paths
through the symbolic execution tree. For example, \texttt{enable} can remain low
for $0, 1, 2, \ldots$ clock cycles between each update to \texttt{state}. Each
of these options represents a separate path through the symbolic execution
tree. This example, although simple, is not all that contrived. It may be that
state in another module of the design can take
varying time to compute an action before \texttt{enable} becomes high again.
%% \cks{and yay! static analysis enables the unsat core
%% heuristic and the segmenting by clock cycles, addressing both problems. Make
%% sure that is made clear later when we refer back to these problems}:
Two problems become apparent:
\begin{enumerate}[noitemsep]
\item The choice of path in the current clock cycle can determine
whether there exists a path in a future clock cycle that will allow the flow
of information to continue.
\item Once exploration starts down one path, it is not clear at what point -- after how many
clock cycles -- the current path should be abandoned as incorrect, and a new
path should be tried. For example, there are infinitely long paths in which
\texttt{prev} never gets to 3 and \texttt{enable} remains low.
\end{enumerate}
\begin{figure}[h]
\centering
\includegraphics[width=\columnwidth,trim = 0 5 0 5, clip]{figures/toy1tree}
\caption{Symbolic execution tree of the design in Figure~\ref{fig:toy1} after
four clock cycles.}
\label{fig:toy1tree}
\end{figure}
%% \cks{Some draft text moved from elsewhere}
%% Taken as input from static analysis tool, e.g., Hyperflow
%% Graph~\cite{andystool}. Shows direct, indirect flows of information with
%% conditions under which the flow occurs. Specifically, each flow in the graph has metadata describing whether
%% the flow happens in a continuous assignment or non-blocking assignment, and a list of the conditions that need to be
%% satisfied for the flow to occur. These conditions are taken from the Verilog source and correspond to a line of code
%% The conditions of the particular if/else statement of that particular line
%% specify the particular flow conditions.
%% \cks{Draft text moved from elsewhere} With each edge also gives information about the line
%% of code at which that particular flow occurs. E.g., for an edge connecting a
%% node for signal $x$ and a node for signal $y$, the edge will list the line
%% of code in which the direct flow $y := x$ represented by this particular
%% edge occurs. Different points of flow will result in different edges, even
%% between the same two nodes. Indirect flows are also represented by edges
%% between the two nodes.
%% \cks{Draft text moved from elsewhere}
%% \cks{Possible Framing: use the ideas of information flow~\cite{denning} and intransitive
%% flows of information~\cite{goguen1982security}. The static analysis finds all
%% points of information flow (connectivity) --
%% it exhaustively enumerates the pairs of signals in the binary information flow
%% relation, direct or indirect. (I think that all pairs found are true elements of the relation
%% assuming there is no dead, unreachable code in the design). The static
%% analysis then implicitly assumes the information flow relation is transitive,
%% building a path for every sequence of information-flow pairs. But the relation
%% is in fact intransitive -- not all paths are realizable paths through the
%% design. We use symbolic execution to enumerate the n-ary information flow
%% relation, using the statically built binary information flow relation as a
%% guide. The intransitive information flow relation as defined by Goguen isn't
%% quite the right fit -- that relation was intransitive b/c it allowed for a
%% mid-point in the flow to be trusted to ``downgrade'' information. What we're
%% talking about is that no such path exists. Maybe the hyperflow graph is better
%% thought of as a binary path-segment relation, rather than information-flow relation. The hyperflow graph assumes the
%% relation is transitive, but it is not and
%% we use symbolic execution to build the true full paths. I changed the name of
%% this section to match this framing. Let's see if that works.}
%%\cks{Some ideas for names: Correlating syntactic flows with information flows, Correlating
%% syntactic data flows with symbolic information flows.}
%% The goal of this work is to amplify the power of static analysis, which is
%% fast/cheap and scales well~\cite{hyperflowgraphs}, but its usefulness to the
%% engineer is limited by over-approximation and the gap between static analysis
%% and generating test cases.
%% To address this gap, we present a novel workflow
%% that uses this information from static analysis to
%% drive symbolic execution of the hardware. By
%% steering execution towards an information flow,
%% we are essentially able to generate a class of
%% execution traces in which a flow into a particular
%% sink is realizable on-the-fly. In other cases, we
%% are able to prove that a given information flow is
%% impossible. To achieve this, we present a novel
%% algorithm to prioritize execution paths to explore and to efficiently search the symbolic execution
%% tree for viable paths.
%% \cks{The example should ideally have statically unrealizable paths, unrealizable
%% paths, realizable paths. It should also be the case that a single static path
%% corresponds to multiple paths through the symbolic execution tree.}
%% \kar{Realizable path: The single-cycle composite flow secret -> temp1 -> out1 is possible, since (enable \& out1\_visible \& enable) is satisfiable.\\
%% Unrealizable path: The composite flow secret -> guard -> out2 is impossible because of an invariant of execution. We always have prev = state - 1, but this flow
%% requires (state == 3) on one clock cycle and (prev == 1) on the next. \\
%% Statically unrealizeable: the flow from secret to temp1 to result (to led) is statically unrealizable, because it would require enable to be true and false at the same time.\\
%% Single static path \& multiple multiple se paths: when secret->temp1->out1 is the IF path, the second if/else statement could take the \texttt{then} or the \texttt{else} branch. This is simpler than showing across two modules... maybe we do want to show that to be more clear about that complexity?}
%% \begin{figure}[h!]
%% \centering
%% \begin{framed}
%% \begin{lstlisting}[style={verilog-style}]
%% module demo (
%% input clk,
%% input enable, out1_visible,
%% input [ 31:0 ] secret,
%% output [7:0] led
%% output [31:0] out1, out2
%% );
%% wire [31:0] temp1 = (enable) ? secret : 0;
%% reg [7:0] result = 0;
%% reg [1:0] state = 0;
%% reg [1:0] prev = 3;
%% reg [31:0] guard = 0;
%% always @(posedge clk) begin
%% if (enable) begin
%% state <= state + 1;
%% prev <= prev + 1;
%% result <= 255;
%% else
%% result <= temp[23:16];
%% end
%% if (state == 3) begin
%% guard <= secret;
%% else
%% guard <= 0;
%% end
%% assign led = result[7:0];
%% assign out1 = (out1_visible & enable) ? temp1 : 0;
%% assign out2 = (prev == 1) ? guard : 0;
%% endmodule
%% \end{lstlisting}
%% \end{framed}
%% \caption{Expository Example.}
%% \label{lst:demo2}
%% \label{fig:demo2}
%% \end{figure}
%% We model the information flow graph as a directed graph $\mathrm{IF} = (V, E)$,
%% where
%% \begin{itemize}[noitemsep]
%% \item $V$ is the set of vertices. Each is labeled with a state-holding
%% variable of the design. There is one vertex per variable. We overload $V$ to
%% be both the set of state-holding variables of the design and set of vertices
%% in the IF graph.
%% \item $E = \mathrm{Exp} \cup \mathrm{Imp}$ is the set of directed edges. Each
%% edge represents a potential flow of
%% information between vertices. Each edge is labled with the line of code at
%% which the flow takes place and the containing constraints. There exist two
%% types of edges, one representing potential explicit flows and one representing
%% potential implicit flows.
%% \end{itemize}
%% For example, in Figure~\ref{fig:toy1ifg}, the edge
%% $(\mathtt{guard},\mathtt{led})$ is in $\mathrm{Exp}$ and the edge $(\mathtt{prev},
%% \mathtt{led})$ is in $\mathrm{Imp}$.
%Outline 0
%% \item The goal is to determine whether the path is realizable or not. \cks{Need an example code with a IF path
%% that is statically feasible -- the conditions are SAT -- but which is
%% unrealizable.} Approach is to use symbolic execution to determine feasibility
%% of the information flow path.
%% \cks{some text we didn't need for DAC, but may be useful here.}
%% We model the symbolic execution of a hardware design in RTL Verilog as a
%% tuple $M = (V, A, S, C, \Pi)$, where
%% \begin{itemize}
%% \item $V = V_I \cup V_S \cup V_C$ The set of variables of the design
%% comprising input variables $V_I$, state-holding, sequential logic variables
%% (\texttt{regs} in Verilog) $V_S$, and non-state-holding
%% variables/combinationa logic signals (\texttt{wires} in Verilog)
%% $V_C$. Output signals are a subset of $V_S \cup V_C$. \cks{Is this true? Are
%% wires ever used as output signals?}
%% \item $A = \{0,1\}^* \cup \Sigma$. The alphabet of concrete values
%% $\{0,1\}^*$ and symbolic values $\Sigma$ (e.g., $\alpha, \beta$) that can
%% be assigned to variables.
%% \item $S: V \rightarrow \phi(A)$ The current state of the symbolic
%% execution, a mapping from variables in the design to expressions/formulas
%% containing/over both concrete and symbolic values/ An assignment of values
%% to the variables/Partial variable assignment. For example, the
%% variable $v \in V$ may have the current state $S(v) = \alpha + 1$. The
%% expressions/formulas use the standard logic, arithmetic, and bitwise
%% expressions defined in Verilog. \cks{use ``context'' instead of state?}
%% Boolean formulas over concrete and symbolic values/variable assignments.
%% \item $\Pi$ The path condition a set of conjuncts describing the
%% constraints over input and state variables. For example $\pi = \alpha <
%% 10$ using standard propositional and first order logic expressions/formulas.
%% \item $C$ represents the RTL Verilog implementing/describing the
%% design. $C$ defines the transition function, which updates either the
%% state or the path condition at each line of code. Each line of code $C \in
%% C$ is either a branch point (e.g., the start of an
%% \texttt{if...then...else} construct) or non-branching. On branching code
%% the path condition $\Pi$ is checked. If $\Pi \rightarrow c$, the
%% \texttt{then} branch is taken. If $\Pi \rightarrow \neg c \not c$, the
%% \texttt{else} branch, if present, is taken. If neither is true, then both
%% branches must be explored in turn/creating two separate paths of
%% exploratin/forking the current ath into two, each of which must then be
%% explroed. To explore the first path, the path condition $\Pi$ is updated:
%% $\Pi:=\Pi \wedge c$, and execution continues down the \texttt{then}
%% branch. To explore the second path, the path condition is updated: $\Pi:=
%% \Pi \wedge \neg c \not c$, and execution continues down the \texttt{else} branch.
%% \end{itemize}
\section{Methodology: Symbolic Execution for Information Flow}
\label{sec:design}
Given a design and an input signal of interest, \texttt{src}, our goal is to
find how information can flow during execution from \texttt{src} through the design. Our approach
is to first use the IF graph to enumerate all potential paths of information flow
through the design from \texttt{src}. As this is a static analysis, complexity
grows linearly with the number of variables in the design and the length of the
RTL code. Then, for each enumerated path, SEIF uses symbolic execution to
either find a corresponding information-flow path through the design, or
determine that no such path exists.
\subsection{Overview}
Once the IF graph is generated, the analysis proceeds in three main phases: pruning globally unrealizable paths,
symbolically executing the design to find realizable paths through the design,
and analyzing the semantics of each found path to find true paths of information
flow. In the following sections, we describe each phase in more detail.
If SEIF returns a path, it is a true path through
the design corresponding to the path in the IF graph. Depending on the
post-processing option used, this will either be a path starting at the design's
reset state or an intermediate state.
If SEIF does not return a path, there are three
possibilities. First, the path in the IF graph has been identified
as infeasible within a bounded number of clock cycles.
Second, the path in the IF graph is
feasible in the design, but does not represent an actual flow of information --
this result is sound with one caveat discussed in
Section~\ref{sec:semantic}. Third, the path in the IF graph cannot be
accounted for. These options are discussed in
Section~\ref{sec:postprocessing} and evaluated in Section~\ref{sec:eval-acctingpaths}.
%The IF graph is used in the first two phases. In the first phase, information taken directly from the IF graph
%can be used to eliminate paths in the IF graph that are unrealizable. These are
%paths that would require mutually contradictory constraints to hold in order to
%be realized. These are globally unrealizable paths because the constraints are
%unsatisfiable regardless of the current state of the design during execution.
%In the second
%phase, we use symbolic execution to find, for each remaining path through the IF
%graph, a corresponding path through the design. Our methodology relies on the hardware-oriented symbolic
%execution engine described in \cite{ryan2023countering}. The number of possible paths
%through the design is large and paths are of unbounded length. The IF graph enables pruning some paths at each clock cycle
%boundary and enables a search heuristic to guide execution toward paths
%more likely to complete the flow of information from \texttt{src}.
%In the third
%phase, we use the symbolic state and path condition from the symbolic execution
%engine to eliminate paths that represent true paths through
%the design, but which do not correspond to a true information flow from \texttt{src}.
\subsection{Pruning Globally Unrealizable Paths from the IF Graph}
\label{sec:pruningglobally}
In the first phase, our goal is to quickly and cheaply eliminate paths through the IF graph that are easily
falsified before moving on to the next, more expensive phase. Consider
the example code in Figure~\ref{fig:toy2}. The variable \texttt{temp} carries the input
\texttt{secret} only when the input signal \texttt{enable} is high. The \texttt{secret}
information is conditionally passed on to \texttt{result} and from there to
\texttt{led2}. The corresponding IF graph is shown in
Figure~\ref{fig:toy2fig}. While the IF graph appears
to show a flow of information from \texttt{secret} to \texttt{led2} via
\texttt{temp}, the constraint for edges (\texttt{secret},
\texttt{temp}) and (\texttt{temp}, \texttt{result}) require \texttt{enable} to be high and low, respectively. Since both edges must occur in the same clock cycle,
this flow cannot be realized.
\begin{figure}[h!]
\centering
\begin{framed}
\begin{lstlisting}[style={verilog-style},belowskip=-.8\baselineskip,aboveskip=-.5\baselineskip]
wire temp = (enable) ? secret : 0;
always @(posedge clk) begin
if (enable) begin
result <= 0;
end else begin
result <= temp;
end
end
assign led2 = result;
\end{lstlisting}
\end{framed}
\caption{A toy example illustrating globally unrealizable paths. \texttt{clk},
\texttt{enable}, and \texttt{secret} are input wires and \texttt{led2} is an
output wire. \texttt{result} is a state-holding reg. \texttt{secret} cannot flow through \texttt{temp} to
\texttt{result} and \texttt{led2}.}
\label{fig:toy2}
\end{figure}
\begin{figure}[h]
\centering
\setlength{\belowcaptionskip}{-5pt}
\includegraphics[scale=.25, trim = -200 150 0 50, clip]{figures/toy2ifg}
\caption{The partial IF graph for the code shown in~\ref{fig:toy2}, showing
only the paths through \texttt{temp}. Although the graph shows a path from
\texttt{secret} to \texttt{led2}, an SMT query finds
that the constraints along the path will never be co-satisfiable.}
\label{fig:toy2fig}
\end{figure}
This analysis requires knowing where clock
cycle boundaries are. In the IF graph, an edge corresponding to a nonblocking
assignment (for example, $\mathtt{result} <=
\mathtt{temp}$) denotes a clock cycle boundary. When \texttt{state} is updated in
one clock cycle, the updated value can be read in the next clock cycle.
At the start of this phase, the given path through the IF is divided into
\emph{segments}.
One segment of an IF-graph path is a sequence of hops in the IF graph.
These hops could be any implicit or explicit flows. However, the explicit non-blocking assignments are of particular interest to us
in determining how we should break the IF path into segments. Each non-blocking assignment
represents exactly where we reach a clock cycle boundary in the IF path and thus
break off a new segment after that flow.
If a path
has $n$ nonblocking assignments, it has $n+1$ segments.
Let us take the following IF path in Figure \ref{fig:toy2fig} as an example:
$\langle (\mathtt{secret}, \mathtt{temp}), (\mathtt{temp},\mathtt{result}),
(\mathtt{result}, \mathtt{led2})\rangle$.
This path has two segments. The first segment is the two-hop sequence,
$\langle (\mathtt{secret}, \mathtt{temp}), (\mathtt{temp},
\mathtt{result})\rangle$, made up of a continuous assignment and a non-blocking assignment.
The second segment, $\langle (\mathtt{result}, \mathtt{led2})\rangle$, is a single hop and a continuous assignment.
For every segment in a given IF-graph path, the conditions
involved in that segment are collected and checked for co-satisfiability. If
the hops in any one segment have mutually contradictory constraints,
that path is discarded. In Figure~\ref{fig:toy2fig}, the segment $\langle
(\mathtt{secret}, \mathtt{temp}), (\mathtt{temp}, \mathtt{result})\rangle$ has
contradictory constraints, as the first hop requires that \texttt{enable} is high, while the second hop requires it to be low.
This pruning analysis is sound---only unrealizable paths are discarded---as long as the co-satisfiability check considers only state-holding signals and input signals in the
satisfiability query, as these signals do not change value in the middle of
a clock cycle.
\subsection{Symbolic Execution to Find Paths through the Design}
In the second phase, the goal is to find true paths through the design for each
remaining path in the IF graph. We use symbolic execution to find
a sequence of
machine states and a corresponding sequence of input signals (for example, as
seen in Figure~\ref{fig:toy1states}) that aligns with the
path outlined by the IF-graph path.
\subsubsection{Symbolic Execution Guided by IF-Graph Path Segments}
The segment analysis done in the first phase provides information about where
the clock cycle boundaries lie; the IF graph also provides information about
which lines of code must execute for each hop in a segment. SEIF uses
this information to drive symbolic execution along the path outlined by the IF graph.
In each clock cycle, the symbolic execution engine is restricted to following only
those design paths which include the lines of code that must be executed for the current
IF-path segment to be realized. For example, in Figure~\ref{fig:toy1}, the
symbolic execution engine only considers paths which take the \texttt{if}
branch at line 8, when $\mathtt{state == 3}$. By doing so, the search space is significantly reduced.
However, there may still be many possible paths through the design to consider,
only some of which allow the complete IF path to be realized. Continuing
with our example, Figure~\ref{fig:se-tree-paths} shows the symbolic execution
tree for one clock cycle of the code in
Figure~\ref{fig:toy1}. Each node in the tree represents a line of code, or non-branching sequence of code (e.g., lines 3-4) to be
executed.
The path of interest, this time annotated with which line of code needs to
execute for each hop to be realized, is $\langle
(\mathtt{secret}, \mathtt{guard})_{\mathrm{line~} 8}, (\mathtt{guard},
\mathtt{led})_{\mathrm{line~} 13}\rangle$. Examining the symbolic execution tree
in Figure~\ref{fig:se-tree-paths}, it would appear that two of the four
possible paths achieve the desired flow. But annotations
in the IF graph tell us that the
sequence of conditions $(\mathtt{state} == 3)_{s3}, (\mathtt{prev} == 3)_{s4}$
needs to be met. For that to happen, lines 3-4 need to
execute in the first four clock cycles and lines 8, 13 need to execute in only
the fourth clock cycle. While this is clear to see when examining the
state transition diagram (Figure~\ref{fig:toy1states}), there is nothing in the IF graph, or even the
code itself, indicating that it will take four clock cycles to realize this flow. Finding the desired path through the multi-clock-cycle symbolic execution tree is a search problem. We discuss the search strategies we developed to guide search in SEIF in Section \ref{sec:strategies}
%% Thus, even after forcing the appropriate conditions in each clock cycle, the
%% resulting tree of paths through the design might still be quite
%% large. The number of paths to explore is still large. Some of those paths will be infeasible. Some of
%% those paths are feasible, but advance the design to a new state in which
%% down-path segments are unrealizable. Sometimes the design must be advanced to a
%% new state before the next segment can be realized. We discuss each of these
%% conditions, and how they are handled, in the next sections.
\begin{figure}[h]
\centering
\setlength{\belowcaptionskip}{-15pt}
\includegraphics[scale=.3,trim= 250 275 425 0,clip]{figures/toy1-se-tree.png}
\caption{Symbolic Execution Tree of Paths}
\label{fig:se-tree-paths}
\end{figure}
%% \cks{Can each subsection be matched to a problem? E.g., infeasible paths in the
%% SE tree,
%% advancing to a state which will make down-path segments unrealizable,
%% advancing to a state required in order to make down-path segments realizable,
%% large search space}
\subsubsection{Pruning Unrealizable Paths at Clock Cycle Boundaries}
As a first strategy, the symbolic execution engine prunes unrealizable
paths at each clock cycle boundary. At each clock cycle, the engine first
checks the co-satisfiability of the conditions required in the current IF
segment, similar to the check done to prune globally unrealizable paths
(Section~\ref{sec:pruningglobally}). However, this time the SMT query
includes the current symbolic state along with the conditions required for the
IF segment. As with the global pruning step, the check considers only the
state-holding variables in the segment conditions, as the value of combinational
logic variables may change during the course of a clock cycle.
Continuing with
our example from Figure~\ref{fig:toy1}, at the start of the initial clock cycle,
the symbolic execution engine checks whether the condition required for the
first hop in the IF graph ($\mathtt{state} == 3$) is
mutually contradictory with the initial symbolic state (in which $\mathtt{state}
== 0$). Indeed, it is, and the symbolic execution engine discards any paths
that would include line 8, the line of code required for the first hop in the IF
graph.\footnote{Discarding these paths can be done prior to exploration of any paths in
the current clock cycle, as the engine has information from the design's
statically built control
flow graph about which lines of code
are included in which path.} At this point, SEIF recognizes that realizing
the first segment of the IF graph at the current state (state $s0$) is infeasible.
\subsubsection{Stalling the IF-Graph Path to Advance to a New Machine State}
\label{sec:stalling}
The second strategy used by SEIF is to pause the search for realizing a
segment of the IF path in order to advance the design to a next-state
when needed. In our example, the first segment of the IF graph cannot be
realized from the initial reset state. SEIF symbolically executes the
design for a single clock cycle, without considering the constraints required by
the next IF path segment, to advance the design to a new state. SEIF then
checks whether the IF graph segment can be realized from this new state.
There are many possible next states and SEIF must find one that satisfies two
criteria:
\begin{enumerate}
\item The next state advances the design toward a state in which the next IF
segment can be realized, and
\item The next state does not undo any prior progress along the IF graph path
that has already been made.
\end{enumerate}
We discuss search strategies for
finding valuable next-states in the next section.
The second constraint is trickier. During normal execution, it is likely that information written to a \texttt{reg} in one clock cycle gets
overwritten in a subsequent clock cycle. For example, consider the code in
Figure~\ref{fig:toystalling}, which is similar to that of our first example
(Figure~\ref{fig:toy1}), but made slightly more complex by the addition of two
new registers: $\mathtt{guard0}$ and $\mathtt{clear}$.
\begin{figure}[h!]
\centering
\setlength{\belowcaptionskip}{-10pt}
\begin{framed}
\begin{lstlisting}[style={verilog-style},belowskip=-.8\baselineskip,aboveskip=-.5\baselineskip]
always @(posedge clk) begin
if (enable) begin
prev <= state;
state <= state + 1;
end
if (state == 0) begin
guard0 <= secret;
end else if (clear) begin
guard0 <= 0;
end else begin
guard0 <= guard0;
end
if (state == 3) begin
guard <= guard0;
end else begin
guard <= 0;
end
end
assign led = (prev == 3) ? guard : 0;
\end{lstlisting}
\end{framed}
\caption{A design demonstrating the challenges of stalling.}
\label{fig:toystalling}
\end{figure}
The IF path of interest is now from \texttt{secret} to \texttt{guard0} to
\texttt{guard} to \texttt{led}. To achieve the second flow segment,
$\langle(\mathtt{guard0},\mathtt{guard})\rangle$, SEIF needs to first
advance the design to a state $s' = \langle\mathtt{state} == 3\rangle$. However, it is
important that while the design advances to state $s'$, the \texttt{clear}
signal is never set, as a 0 written to \texttt{guard0} would undo the information flow from \texttt{secret} to
\texttt{guard0} from the prior IF path segment.
SEIF uses information from the IF graph to \emph{stall}
the information flow while advancing the design to a next-state. We define
stalling as symbolically executing the design for a single clock cycle, such that
the design transitions to a next state, but the position along the IF path
remains unchanged. To stall, SEIF prevents the symbolic execution engine from considering any paths of
execution that will undo information flow from prior segments in the IF
path. To do this, SEIF considers the node $n$ in the IF path, in which information
currently ``resides.'' In our current example, this would be the node
\texttt{guard0}. SEIF then uses the IF graph to find all edges incident to node
$n$, which represent flows of information from variables in the design to $n$ and are associated with lines of code. Explicit
flows need to be prevented during stalling, but implicit
flows do not need to be prevented, as they do not cause the value in $n$ to be overwritten. SEIF avoids exploration of any paths through
the design which would execute a line of code in which $n$ is written to. In
this way, the information in $n$ is not lost while stalling.
There are two edge cases to consider. The first is self-loops. Direct flows from $n$ to $n$ (e.g.,
$\mathtt{n} <= \mathtt{n} + 1$ are
allowed, as the information in $n$ stays in $n$. The second is the case when $n$
is assigned a constant (e.g., $\mathtt{n} <= 1$). SEIF
checks this corner case during symbolic execution and abandons any path in
which it occurs. If the assignment by a constant happens regardless of the rest of the state,
then stalling cannot occur at this point in the IF graph.
Because of stalling, the number of clock cycles needed to verify the information flow
may exceed the length of the IF path.
%% The symbolic execution engine must find a path through the SE
%% tree such that the leaf node corresponds to a useful next-state in the state
%% transition diagram of the design, and the current position in the IF-graph path
%% has not changed.
%% To do this the symbolic execution engine leverages information from the IF
%% graph. \cks{What are the conditions for excluding paths when stalling? Lines of
%% code that write to the variable which is the last node in the current segment
%% need to be excluded, but if the variable is writing to itself, that is ok. Any
%% other exceptions? From the graph we know all edges incident to the node of
%% interest. And for each edge, we know the line of code associated with it. We
%% exclude any paths that include that line of code. What about when the last hop
%% in a segment is an implicit flow?}
%% During the preprocessing step, our goal was to identify all the flow conditions for each signal
%% along our information flow path. In addition, for each register in the flow path,
%% we need to know all flows into the register which
%% are not part of the particular flow in question.
%% When we want to hold the information flow in
%% a particular register during execution, we need
%% to turn off all such flows, or \textit{stall}.
%% When we stall, the design is (symbolically) executed for one
%% clock cycle. The symbolic execution is guided such that information that has flown to
%% a signal that is a mid-point between source and sink does not get
%% overwritten during this execution.
%Because of stalling, the number of segments in the information flow path, not
%including any tail segment,
%determines only the minimum number of
% clock cycles of simulation needed to verify the information flow. More cycles may be required.
%This is necessary for our stalling step, or for when we want to hold
%the information flow in a particular register during execution. We need to know all such flows, in order to
%``turn them off''/stall even if these flows are not part of the particular composite information flow path in question.
%% %\kar{this is from matthew's paper}
%% When symbolically executing the design, we
%% start from a fully symbolic state. Since a fully
%% symbolic state has no restrictions, this simplifies our approach. We only have
%% to consider flows that move information from the
%% initial symbol in the source register to the sink in question. It’s possible that, if we continue execution, we are able to find flows starting after the
%% first clock cycle. But because the fully symbolic
%% state is unrestricted, these flows are necessarily
%% special cases of flows we would be able to find
%% in fewer clock cycles of simulation. This helps to
%% mitigate the path explosion problem.
%% Starting from a fully symbolic state means that
%% we generate path suffixes, instead of full execution
%% paths from a reset state. This has two important
%% implications. First, it completely eliminates false
%% negatives from our analysis. That is, if we elimi-
%% nate an information flow path from our consider-
%% ation, it cannot be realized in any execution trace.
%% However, the reverse is not necessarily true: if
%% we determine that a flow is indeed possible, it
%% could be the case that the path suffix containing
%% the flow started from an unreachable state. If the final path
%% condition constrains the starting state to include
%% at least one reachable state, then we have a true
%% positive result.
%% This decision offers several advantages over
%% starting execution from a reset state. If we start
%% execution from reset, we can’t guarantee that the
%% information flow will start in the first clock cycle
%% of execution, as the design may have a reset cycle
%% that requires many clock cycles before it reaches
%% a standard operating state. This means we have
%% to keep track of information flows from every
%% value the source signal takes on in every clock
%% cycle. In addition, this prevents elimination of
%% paths in which an intermediary tainted register is overwritten while stalling. This is because the new
%% data may in fact represent a new flow along the
%% same flow path.
\subsubsection{Search Strategies}
\label{sec:strategies}
The goal is to find a sequence of design states, and corresponding
input values, that correspond to an IF path, or determine that
no such sequence exists. The search space is large; an IF path with $n$ segments
requires at least $n$ clock cycles through the design. When stalling is
needed, the number of clock cycles required is
unbounded (although finite).
Information from the IF graph is used to prune the symbolic execution tree at each clock cycle, but a single IF hop can correspond to many paths through the symbolic
execution tree. This is because a segment of the IF-path involves only a small number (typically
fewer than 5) of lines of code be executed. The input space is partially
constrained to ensure
those few lines of code are executed, but most of the input space is unconstrained,
and therefore there is freedom in how most of the design is explored at each
clock cycle.
%And a poorly chosen path through the design in an early clock
%cycle may preclude successfully finding a needed path through the design in a
%later clock cycle.
%\kar{cut this?} Additionally, at each clock cycle it may be the case that information flow can stall
%for an arbitrary or fixed amount of time. In other words, the IF-path can
%stutter while the design continues to execute for some number of clock
%cycles, and then the IF-path is picked back up again.
We developed and implemented four search strategies:
\begin{itemize}
\item Baseline 1 -- Continue / Stall Only.
\item Baseline 2 -- Backtracking Only
\item Stalling with Backtracking
\item Stalling with UNSAT Core Heuristic
\end{itemize}
\paragraph{\textbf{Baseline 1: Continue / Stall Only}}
\label{sec:baseline-1}
The key idea behind this strategy is that, for each segment, we can either symbolically
execute until a design path is found in which the segment conditions are
satisfied (termed a \emph{continue}), or we can stall for some bounded number of cycles. For an IF path, we build and exhaustively search a list of all possible \emph{continue}, \emph{stall}
combinations. If SEIF is unable to complete the IF path for a given
continue-stall pattern, it moves on to the
next pattern. The list of continue-stall combinations are in truth-table order to allow the SEIF
engine to explore as deeply as possible first, aiming to verify the shortest path possible with no stalls.
In this context, depth equates to the number of IF-path segments successfully
traversed, and for which SEIF has realized a partial path of execution.
%then there are two options: stall or backtrack. Use heuristics \cks{from the unsat core we think}to determine which option to chose.
%\item If stalling, choose one of CCSC, CSCC, etc. and either start the
%search fresh, this time with a stall cycle in between two continue cycles,
%or go back to an earlier clock cycle in this search and add a stall
%cycle. Our strategy proceeds in truth-table order. \kar{need to explain better probably}
%\item With this truth-table ordering, we go deep as possible first. The idea being that we may as well try for
%the shortest possible path with no stalls first. In this context, we mean depth to mean the number of information
% flow segments successfully traversed, and for which we have a path through the symbolic execution tree. We have
% found realizable paths through the design for these partial flows. Breadth in this context through a symbolic execution
% tree would be exploring all of the paths until we find one that produces the necessary flow for a particular information
% flow segment.
%\item Once all SE paths for this cc have been explored and none
% have produced the information flow that we desire for this IF-path
% segment, then we know we need to either a) find a different SE path in
% one of the earlier clock cycles or b) stall somewhere along the
% IF-path -- maybe here or maybe earlier. The order we proceed in is defined for us -- truth-table.
\paragraph{\textbf{Baseline 2: Backtracking Only}}
In this search strategy SEIF
begins by symbolically executing for one clock cycle for the first segment. If the flow found, SEIF
moves to the next segment in the IF path. If at any segment, the flow is not found in some bounded number
of clock cycles, or there are no more design paths to try, SEIF returns (or \emph{backtracks}) to an earlier
segment to find a different path that satisfies the same segment conditions.
%Some bookkeeping is done here to be able to re-search the second clock cycle to look for a new path
%without repeating work, too. \kar{explain}
% \begin{itemize}
%\item Go back to an earlier clock cycle to look for a different path that satisfies
%the same IF-path-segment flow requirement.
%\item If backtracking, go back to the prior clock cycle and look for a
% second path in which the leaf node shows that information has flown from
% $x$ to $y$ -- again, not looking at leaf nodes, just whether or not a line
% of code has been executed. Some bookkeeping is needed to be able to re-search the second
% clock cycle to look for a new path without repeating work.
% \end{itemize}
\paragraph{\textbf{Stalling with Backtracking}}
This strategy is a hybrid of baselines 1 and 2.
For any given \emph{continue}, \emph{stall} pattern, after successfully
executing consecutive \emph{continues}, and reaching a \emph{stall}, SEIF
stalls for a bounded number of clock cycles and
attempts to find execution paths where SEIF can make forward progress in the next segments. If all symbolic execution paths are explored, or SEIF times out (according to some pre-determined bound), it backtracks.
\paragraph{\textbf{Stalling with Heuristic}}
\label{sec:unsat}
This strategy builds on top of stalling with backtracking. Our heuristic
relies on the \emph{UNSAT core}, the subset of constraints in a SAT query for
which no satisfying assignment exists. If SEIF stalls, it is searching for a
new machine state that will satisfy the conditions of the next IF path segment.
In this case, SEIF pushes the symbolic state and the constraints from the next
segment to the SMT solver, which returns the UNSAT core. %% From these constraints we derive the UNSAT core, which helps to find a path in the design that (1) corresponds to a stall of the information flow, and (2) makes
%% forward progress along the IF flow path. To do this, after stalling,
For each path explored while stalling, SEIF checks if the
UNSAT core became smaller. If it did, SEIF continues searching for a new
machine state along the path. If it grows, SEIF prioritize the next candidate stall path.
\subsubsection{Post Processing to Find Reset}
\label{sec:postprocessing}
SEIF begins exploration from a symbolic state, and therefore the
design paths it generates inputs for may not start from the
reset state. We mitigate this by checking whether the found
design path has constraints that conflict with the design's reset
state. If not, the path can start from reset. If so, the path
starts from an intermediate state of the design, and SEIF cannot
guarantee that it is a reachable state. Most often, SEIF finds paths that
can start from reset and we evaluate this in Section~\ref{sec:eval-acctingpaths}.
\subsection{Semantic Analysis to Identify True Information Flows}
\label{sec:semantic}
Once per execution path, SEIF performs a semantic analysis check to prune
flows that represent viable design paths, but not true flows of information.
This can happen when a textual flow does not represent an information flow. For example, \texttt{y <= x xor x}, would yield a path showing x flows
to y even though there is no flow from x to y. SEIF prunes explicit textual
flows which do not represent information flows.
If there is an implicit textual flow that is not a true information flow, SEIF cannot eliminate
that false positive. For example, \texttt{if (x XOR x) y <= 0; else y <= 1;}
(Here, there is no path in which \texttt{y} is set to 0, and SEIF does recognize
that.)
%% \begin{figure}[h]
%% \centering
%% \begin{subfigure}[b]{0.2\textwidth}
%% % \begin{framed}
%% \begin{lstlisting}% [linewidth=.2pt,style={verilog-style},belowskip=-.8\baselineskip,aboveskip=-.5\baselineskip]
%% x
%% \end{lstlisting}
%% % \end{framed}
%% \caption{Implicit textual flow}%An implicit textual flow that is not a true flow of information.}
%% \label{fig:text-flow}
%% \end{subfigure}
%% \begin{subfigure}[b]{0.2\textwidth}
%% % \setlength{\belowcaptionskip}{-10pt}
%% \includegraphics[scale = 0.3, trim = 30 0 40 10, clip]{figures/reconvergent.png}
%% \caption{Reconvergent flows}
%% \label{fig:reconvergent}
%% \end{subfigure}
%% \caption{Textual information flows}
%% \label{fig:semantic-if-flows}
%% \end{figure}
%% \vspace{-10pt}
In the case of reconvergent fan-out SEIF may or may not find the flow. In
the example of Figure \ref{fig:reconvergent}, \texttt{x} is an input and blocks 2 and
3 represent different areas of the design (i.e. modules, always blocks). There are 4
cases to consider:
\begin{enumerate}
\item The writes to \texttt{y} and \texttt{y'} are both unconditional and there is no flow from \texttt{x} to \texttt{z} because $\mathtt{z} = 3\mathtt{x} - 3\mathtt{x}$.
SEIF performs the check and correctly detects no flow.
\item The writes to \texttt{y} and \texttt{y'} are conditional, and depend on
the same conditions. SEIF detects there is no flow
\item The write to \texttt{y'} is conditioned on something that is mutually UNSAT with the condition for \texttt{y}. In this case, there
is always a flow from \texttt{x} into \texttt{z}, and SEIF detects it.
\item The write to \texttt{y'} is conditioned on something mutually satisfiable with the condition for \texttt{y}, where the condition
for \texttt{y} is different. If SEIF follows a design path where both conditions are true at the same time, it detects no flow,
while there may be other design paths through block 3 which would enable a flow,
and vice-versa. Unless SEIF is able
to exhaustively explore, it may report an incorrect result.
\end{enumerate}
\vspace{-5pt}
\begin{figure}[h]
\centering
\includegraphics[scale = 0.3, trim = 30 0 40 10, clip]{figures/reconvergent.png}
\caption{Reconvergent flows}
\label{fig:reconvergent}
\end{figure}
\vspace{-10pt}
%In the case of an implicit flow at the textual/signal level from $x$ to $y$, but
%where there is no flow at the semantic level, we do not differentiate.
\section{Implementation}
We implemented SEIF using the Sylvia symbolic execution
engine~\cite{ryan2023countering} and using hyperflow
graphs~\cite{meza2023hyperflowgraph} as our IF graph engine.\footnote{We
contacted the authors of the hyperflow graph paper and they gave us closed-box
access to the tool, providing the static analysis for the designs we gave
them. The
authors of the Sylvia symbolic execution engine gave us source-code access to
their tool.} Both Sylvia and
the hyperflow graph toolchain were built using python3. Sylvia
implements the Verilog semantics according to the
IEEE 1364-2005 semantics using pyVerilog and the Z3 solver for SMT solving. SEIF
also uses Z3 for preprocessing and path removal.
When considering information flow paths that span multiple modules, enumerating all possible
paths for even a single source/sink pair becomes too
expensive. We manage this complexity by following the divide-and-conquer
approach of Ryan et al.~\cite{ryan2023countering}.
SEIF first finds the partial IF paths within a module, and then uses the segment
conditions to find the next module to explore. SEIF uses the SMT solver to ensure that the path fragments can be stitched back together to form a valid information flow path from source to sink.
This approach reduces repeated work within
a module when exploring paths across multiple modules.
\section{Evaluation}
\label{sec:eval}
We evaluate SEIF over four open-source designs to study its viability
as a means for accounting for information flows within a hardware design. The evaluation
addresses the following questions: 1) Can SEIF recognize and eliminate paths
through the IF graph that are unrealizeable in practice?
2) Can SEIF find paths through the design,
along with the sequence of inputs to realize the path, that corresponds to paths through the IF graph?
3) Can SEIF be meaningfully applied to security relevant signals in hardware
designs to give experts
feedback on the security of the design or new areas to explore?
\subsection{Dataset and Experimental Setup}
We collected four open-source Verilog designs for evaluation. The designs are:
\begin{enumerate}
\item OR1200, a 5-stage RISC processor core~\cite{or1200};
\item openMSP430, a synthesizable 16-bit microcontroller core~\cite{msp430};
\item the AKER Acess Control Wrapper (ACW) \cite{restuccia2021aker}; and
\item an AES implementation from TrustHub \cite{TrustHub1} \cite{TrustHub2}.
\end{enumerate}
The experiments are performed on a machine with an Intel Xeon E5-2620 V3 12-core
CPU (2.40GHz, a dual-socket server) and 62G of available RAM.
%% In the following sections we For each design we provide some performance metrics, statistics to answer the research questions above, and security analysis
%% focused on the specific security critical signals or properties of interest.
\subsection{Accounting for Paths in the IF Graph}
\label{sec:eval-acctingpaths}
We first examine SEIF's ability to account for paths in the IF graph,
either by finding paths through the design that correspond to the IF path, or by
eliminating the IF path as infeasible. In these experiments we look at the OR1200, MPS430, and ACW
designs, which are the largest of the four.
We identified 20 security-critical signals in the OR1200 to use in our experiments that appear in
security properties of the OR1200 collected from the security literature \cite{hicks2015specs} \cite{bilzor2011security} \cite{zhang2017scifinder} \cite{zhang2020transys} \cite{trippel2020ICAS}. We selected 10 sources to analyze in the MSP430 by finding signals roughly analogous to those in the security properties for the OR1200.
For the ACW, we chose 20 main internal signals to look at that appear in the security properties manually and automatically generated by \cite{restuccia2022framework} \cite{Deutschbein2022JCEN} and map to several known CWEs.
For each source signal there can be tens of thousands of IF paths. (See the numbers in Tables~\ref{lst:security-analysis-msp430}
and~\ref{lst:security-analysis}, discussed in Section~\ref{sec:security-analysis}.) For the efficacy
and performance evaluations in this and the next two sections, we analyze a subset
of the total paths. For each source signal of interest, we randomly selected 300
paths from the IF graph for analysis. For the security analysis case study
(Section~\ref{sec:security-analysis}), we analyze all paths from a given source.
%\subsection{Accounting for Information Flows}
%% For the OR1200 and ACW, we first identify security critical sources, and then we choose 300 random paths to perform the information flow analysis. The numbers in the table
%% represent the average taken over all sources.
Figure~\ref{fig:accounting} summarizes SEIF's ability to account for the IF
paths.
For 86\% to 90\% IF paths on average, SEIF either finds the corresponding path through the
design or eliminates the IF path as infeasible or not representing a true flow
of information. The majority of accounted-for IF paths, 58\% to 77\% on
average in the three designs, are true paths in the design, indicating that the
static analysis done to build the IF graph is a decent approximation of
information flow through the design. We further break down these
numbers to show the percentage of the found IF paths for which SEIF returns a
design path that starts at the reset state vs. a design path that starts at some
intermediate state. Paths that start at the reset state are better for the
engineer as they can be immediately replayed from the known reset state.
\begin{figure}[h]
\centering
\setlength{\belowcaptionskip}{-5pt}
\includegraphics[scale=0.28, trim = 0 20 0 55,clip]{figures/accounting.png}
\caption{Accounting for IF Paths}
\label{fig:accounting}
\end{figure}
\subsection{Evaluation of Search Strategies}
In the following we evaluate the four search strategies discussed in
Section~\ref{sec:strategies}. Figure~\ref{fig:findflows-percent} reports, for
each design, the percentage of IF paths found by each of the four search
strategies. These are paths for which SEIF found a corresponding path through
the design. As expected, the heuristic
guided search outperforms the other strategies in all three designs, improving
over the baselines by 26\% on average and over bounded stalling with
backtracking by 11\% on average. We note that baseline 2, which does
not include stalling, is the least successful at finding corresponding paths in
the design. This highlights the value of SEIF: many IF paths give an incomplete
picture of a path through the design and include points where the design must advance to
a new state before the IF path can continue. Without SEIF, it would be up to the engineers to
figure out how and whether to advance the design state.
\begin{figure}[h]
\centering
\includegraphics[scale=0.35,trim = 0 20 0 55,clip]{figures/findflows-percent.png}
\caption{Finding Design Paths Corresponding to IF Paths}
\label{fig:findflows-percent}
\end{figure}
Figures~\ref{fig:findflows-time} and \ref{fig:findflows-cc} report on the
performance of the four search strategies, both in terms of average time taken to
find a corresponding design path and average number of clock
cycles through the design for the found path. Again, the
heuristic guided search outperforms the other strategies, completing the search
for each IF path in 3-6 seconds.
\begin{figure}[h]
\setlength{\belowcaptionskip}{-5pt}
\centering
\includegraphics[scale=0.35,trim = 0 20 0 55,clip]{figures/findflows-time.png}
\caption{Time to Find Design Paths}
\label{fig:findflows-time}
\end{figure}
\begin{figure}[h]
\setlength{\belowcaptionskip}{-5pt}
\centering
\includegraphics[scale=0.35,trim = 0 20 0 55,clip]{figures/findflows-cc.png}
\caption{Clock Cycles to Find Design Paths}
\label{fig:findflows-cc}
\end{figure}
Figure~\ref{fig:backtracking-freq} shows that the amount of backtracking that is
required is lowered when we incorporate bounded stalling. Adding the heuristic
improves the efficacy of stalling and therefore decreases backtracking even further.
\begin{figure}[h]
\setlength{\belowcaptionskip}{-10pt}
\centering
\includegraphics[scale=0.35,trim = 0 20 0 55,clip]{figures/backtracking-freq.png}
\caption{Frequency of Backtracking}
\label{fig:backtracking-freq}
\end{figure}
%% how well SEIF performs with the four heuristic-guided search strategy
%% Figures \ref{fig:findflows-percent}, \ref{fig:findflows-time},
%% \ref{fig:findflows-cc}, \ref{fig:backtracking-freq} and \ref{fig:accounting}
%% summarize our the methodology's ability to find information flows. For 300
%% randomly selected paths for each of the security critical sources, we
%% attempted to verify the information flow path. We report the average \% of
%% flows found, clock cycles necessary to find the flow and time taken. This was
%% repeated for each of the 4 search strategies/heuristics.
To better understand how SEIF is finding flows over time, we explore all
IF paths from a single source signal, the program counter, in
the MSP430. We track how many IF paths are found in the design after 1 clock
cycle of search, 2 clock cycles of search, etc. The experiment was done with
heuristic-guided stalling turned on. Figure~\ref{fig:flows-overtime}
shows the results. There were a total of 19060 IF paths, and SEIF
found design paths for 89.93\% of them. The complete search took 16 clock
cycles, however, most of the paths were found withing the first 8 clock
cycles. The experiment took 3.5 days to run.
\begin{figure}[h]
\setlength{\belowcaptionskip}{-10pt}
\centering
% \includegraphics[scale = 0.45]{figures/bd-stalling-graph.png}
\includegraphics[scale=0.35,trim = 0 20 0 65,clip]{figures/accounting-msp430.png}
\caption{Finding design paths over time}%corresponding to IF paths from the program counter in the MSP430 over time}
\label{fig:flows-overtime}
\end{figure}
\subsubsection{Determining the Stall Bound}
For all the experiments in the previous sections, the number of stalls per IF
path segment was set to be
5, 5, and 4 for baseline 1, bounded stalling with backtracking and the UNSAT core heuristic, respectively.
(As a reminder, baseline 2 is backtracking only, with no stalling).
We determined these numbers empirically by selecting at random 5 of the
security-critical source signals from the OR1200, and for each of these source
signals selecting at random 300 paths to evaluate, and then running the experiments with an
increasing number of stalls allowed until we saw the number of IF paths found
begin to flatten out. Finding the bound for the heuristic-guided stalling
strategy is shown in Figure \ref{fig:stalling-unsat-graph}. The graphs
for the other three search strategies are in the appendix.
%\begin{figure}[h]
% \centering
% \includegraphics[width=\columnwidth,trim = 0 20 0 55,clip]{figures/baseline1-stalling-graph.png}
%\caption{Empirically determining the stall
% bound for baseline 1.}
% \label{fig:baseline1-graph}
%\end{figure}
%\begin{figure}[h]
% \centering
% \includegraphics[scale = 0.45]{figures/bd-stalling-graph.png}
% \includegraphics[width=\columnwidth,trim = 0 20 0 65,clip]{figures/bd-stalling-graph.png}
%\caption{Empirically determining the stall
% bound for bounded stalling with backtracking.}
% \label{fig:bd-stalling-graph}
%\end{figure}
\begin{figure}[h]
\centering
\setlength{\belowcaptionskip}{-15pt}
% \includegraphics[scale = 0.45]{figures/bd-stalling-graph.png}
\includegraphics[scale=0.38, trim = 0 20 0 65,clip]{figures/stalling-unsat-graph.png}
\caption{Finding the stall
bound.}
\label{fig:stalling-unsat-graph}
\end{figure}
\subsection{Eliminating Information Flows Paths}
We examine how IF paths that do not correspond to information-flow paths
through the design are falsified in Figure~\ref{fig:falsified}. The experiment used the 300
randomly chosen paths for the 20 security-critical signals in the OR1200. The
largest percentage of eliminated paths are found statically before symbolic
execution begins. This is good news, as that is the cheapest and quickest phase
of the analysis. There is a non-trivial portion, 5\% to 7\%, that are eliminated because they do not represent
true flows of information through the design. SEIF's use of symbolic execution
allows for this precise analysis, which taint tracking may not be able to
provide.
\begin{figure}[h]
\setlength{\belowcaptionskip}{-10pt}
\centering
% \includegraphics[scale = 0.45]{figures/bd-stalling-graph.png}
\includegraphics[scale=0.38,trim = 0 20 0 55,clip]{figures/falsified.png}
\caption{Breakdown of how flows are falsified by SEIF}
\label{fig:falsified}
\end{figure}
%% \cks{Maybe this is totally redundant information with
%% Figure~\ref{fig:accounting}. Cut?}
%% In Figure \ref{fig:replay}, we report the average number of information flows we still find to be viable after our pruning passes
%% and how many we find to be repayable from the reset state in the OR1200.
%% \begin{figure}[h]
%% \centering
%% % \includegraphics[scale = 0.45]{figures/bd-stalling-graph.png}
%% \includegraphics[width=\columnwidth,trim = 0 20 0 55,clip]{figures/replay.png}
%% \caption{Finding replayable information flow paths}
%% \label{fig:replay}
%% \end{figure}
\subsection{Case Study: Security Property Verification}
\label{sec:security-analysis}
When starting with a property, such as is often done in security verification
tasks, SEIF goes beyond producing a single counterexample. In traditional,
assertion-based formal methods, once the formal or bit-level engine produces the first counterexample, it takes manual manipulation of the property
or environment to generate subsequent violating traces.
SEIF is able find multiple realizable traces through the design that exhibit the vulnerable behavior and
can guide the security engineer to other areas of the design they may be interested in exploring.
We demonstrate the approach for two security-critical properties from the TrustHub
Security Property/Rule Database~\cite{TrustHub1, TrustHub2}, one for the MSP430
and one for an AES implementation. The MSP430 property asserts that the program counter’s value should not be readable
from the debug access port during normal operation. %% This is a case where information, or a security asset, should
%% not be transmitted across certain module boundaries under certain conditions.
The AES property verifies that the secret key material is not accessible to any
unprivileged internal data registers \cite{zhang2021sidechannel}.
SEIF generates all the paths from the source of interest to the security-critical sink automatically.
In order to produce the violating paths,
SEIF adds a constraint to the solver specifying the desired precondition.
If we find a candidate violation
of the security property, we ensure it is replayable from the reset state of the
design. The results for the MSP430 and AES are presented in
Tables~\ref{lst:security-analysis-msp430} and \ref{lst:security-analysis}, respectively.
%Our methodology would allow a security engineer to quickly enumerate the ports in the frontend module where the program counter originated, and the debug module, and find information flow paths between any of the source/sink pairs, beyond the original two that we identified in the property.
%We can symbolically execute any one of these paths, and if we successfully find the flow, then we can send the path condition to the solver and it will generate the constraints we need to realize that path concretely. However, this set of paths is a superset of the paths that actually violate the property, during this exploration phase we were not taking into account this precondition -- ``during normal operation.'' The solution is to add an additional constraint to our solver before finding that concrete input trace specifying the desired precondition.
\begin{table}[htb]
\small
\centering
\begin{tabular}{rr}
\toprule
Metric & Result \\
\midrule
Total IF paths from source: & 19060 \\
Total sinks reachable from source: & 41 \\
Total IF paths violating security property: & 58 \\
Avg. time to produce a counterexample (s): & 0.678 \\
Avg. no of clock cycles explored: & 8.13 \\
Total realizable paths violating security property: & 46 \\
\bottomrule
\end{tabular}
\caption{Security Property Verification: Program Counter in MSP430}
\label{lst:security-analysis-msp430}
\end{table}
\begin{table}[htb]
\small
\centering
\begin{tabular}{rr}
\toprule
Metric & Result \\
\midrule
Total IF paths from source: & 61639 \\
Total sinks reachable from source: & 39 \\
Total IF paths from source violating security property: & 57 \\
Avg. time to produce a counterexample (s): & 0.505 \\
Avg. no of clock cycles explored: & 4.102 \\
Total realizable paths violating security property: & 25 \\
\bottomrule
\end{tabular}
\caption{Security Property Verification: Secret Key in AES Implementation}
\label{lst:security-analysis}
\end{table}
%% \subsection{Comparison to Current State of the Art}
%% Currently, the state of the art in any hardware security verification task is property-based.
%% This approach limits any methodology's usage to experts that a) know the design well enough to write
%% high-quality security properties or b) limits the reach of the verification activity to whatever is specified
%% by the particular property. Our methodology represents a new area in the design space and addresses these two concerns.
%% %In addition to being property-based, the state of the art in information flow analysis is done by commercial tools, where the
%% %the methodology is quite manual. For example, with these property-based tools, like Cadence JasperGold SPV, once you find a path or information flow,
%% %it is not immediately apparent how to tell if there exist more paths, or how many more. Our methodology can quickly find the next counterexample involving a source/sink pair
%% %by testing the next candidate paths, whereas JasperGold would require the engineer to manually edit a property or change bits in conditions.
%% In Section \ref{sec:security-analysis} we discuss how our methodology can be used to find security relevant flows that were also found by JasperGold SPV. However, the waveforms produced by JasperGold only produce single counterexamples, not a set of candidate paths. In terms of a performance evaluation, we have access to JasperGold SPV, but their software license unfortunately prevents head-to-head comparisons in published research.
%% EISec extracts a model from symbolic execution in order to exhaustively check security properties of hardware designs \cite{fowze2022eisec}. This is a property-based approach that enumerates vulnerable states in a model of the hardware design in order to find violations. While they analyze several lightweight cryptographic modules and a RISC controller, no data is available on the size of these modules or how long the tool takes to run.
%% Knox is framework for verifying the security of hardware designs \cite{athalye2022knox}. They are concerned with the verification of software running on hardware, and they use the Notary \cite{athalye2019notary} toolchain to convert C and Verilog to models compatible with the Rosette symbolic execution engine \cite{torlak2014rosette}. The authors report runtimes of 217 minutes, 78 minutes and 52 minutes to verify designs that contain 2860, 3260 and 331 lines of code, respectively. This does not include the time needed by the user / designer to manually write the proof artifacts or construct the specifications.
%% Work by Cherupalli et al. uses symbolic simulation to verify information flows in binaries running on hardware \cite{cherupalli2017software}. They run a set of
%% symbolic gate-level information flow tracking benchmarks with the MSP430. \kar{I don't understand what's happening in this paper / how to make sense of the results}
%The introduction puts this work
%against~\cite{athalye2022knox,fowze2022eisec,cherupalli2017software,athalye2019notary}. The
%evaluation should mention those papers. \kar{done}
% \begin{table*}[htb]
% \small
% \centering
%\begin{tabular}{p{1.2in}rrrr}
% \toprule
% Configuration & \multicolumn{1}{c}{Total paths before pruning} & \multicolumn{1}{c}{Total paths after} & \multicolumn{1}{c}{Replayable paths} \\
% \midrule
%Baseline 1 & 300 & 197.94 & 177.12 \\
%Baseline 2 & 300 & 178.30 & 152.34 \\
%Stalling w/ Backtracking & 300 & 217.02 & 212.12 \\
%Stalling with Heuristic & 300 & 239.33 & 231.21 \\
% \bottomrule
%\end{tabular}
%\caption{Replayability of Paths in the OR1200}
%\label{lst:replay}
%\end{table*}
%\subsection{Open Titan}
%\cks{If Andy et al. used their static IF analysis to find the
%error in RndCnstKey in OpenTitan, perhaps we could show how much easier that
%analysis would be with all the FP flows eliminated.}
%In Andy's DAC submission, they look at the OTP controller. Finding paths from
%OTP to AES core. All paths found are realizable. Tainting memory of OTP memory
%and all keys in the crypto modules. The hyperflow graph has 11,579 vertices
%(wires, registers, variables) and 32,084 edges (potential IF flows). 27,218
%explicit and 4,866 implicit. Simulating the entire OpenTitan. Using OTP
%controller ``smoke test''. There were two outputs that appear to be connected to
%RNDCNSTKEY in the hyperflowgraph, but for which the testbench did not show the
%path. This is another use of SE. Even though no false positives in this
%hyperflow graph (or at least none of the paths of interest that they looked at
%had FPs) there are some paths that couldn't be found through standard
%testbenching and had to be manually analyzed. SE could find them.
%Andy found 2 half-paths that each made 26 hops out of a total of 78 edges. Can
%we find the rest of the path?\\
%source port: rnd\_cnst\_key\\
%destination ports: /ot\_top/u\_otp\_ctrl/intr\_otp\_error\_o\\
%/ot\_top/u\_otp\_ctrl/intr\_otp\_operation\_done\_o
%As demonstrated in the sections above, we can take a complex
%design, look at all possible paths and rule out some paths and find a good
%proportion of realizable ones. Demonstrate useful to security with use cases:
%esigns and properties. Technique allows us to do a security task -- IF analysis
%--at a scale that other tools have not been able to achieve before. IF analysis is done by
%commercial tools but is very manual.
%Look at signals of architectural significance to make it easier to interpret the
%results. E.g., key register to output port, want to know confidentiality is not broken.
%\subsection{Evaluation Questions (Notes from Meeting with Intel)}
%Talk about the paths found to be unrealizable
%\begin{itemize}
%\item What did they look like?
%\item What was the condition that turned out to be unrealized?
%\item What was the structure of the path/code that leads to IF path, but is
% not an actual path through the design? At the syntactic level.
%\item At a high level -- what are the structural design aspects that led to
% falsified paths? Do there exist design patterns that lead to falsified paths?
%\end{itemize}
%How many SMT queries are we talking about?
%\begin{itemize}
%item if 5k paths are eliminated, did it take 5k queries?
%\item does one early UNSAT result enable eliminating lots of down-path
% branches
%\item there may be room to improve here -- if one path is falsified, then others
% with the same prefix are also falsified.
%\end{itemize}
%\subsection{Evaluation Cases (Notes from 4/5 meeting)}
%\begin{itemize}
%\item Baseline1: continue, stall in truth-table ordering with no backtracking
%\item Baseline2: never stall, always backtrack (this can exhaustively complete)
%\item Bounded stalling with backtracking: still using truth table ordering. when stuck, stall up to 5 clock cycles and then backtrack
%\item Stalling w/heuristic: when stuck, stall up to 5 clock cycles with happy faces%
%and then backtrack. At the first sad face, backtrack. This is bounded stalling but
%with an early exit to backtracking, according to the heuristic.
%\end{itemize}
%Search is DFS
%Evaluation to do
%\begin{itemize}
% \item randomly choose 300 paths to work with when figuring out a good bound
%\item increasing bound in baseline1 case to find a good bound. keep increasing bound
%until the percentage of flows accounted for no longer improves
%\item implement Baseline2
%\item find a good bound to use with bounded stalling with backtracking.
%\item find a good bound to use with heuristic-guided stalling with backtracking.
%\end{itemize}
%For paths we find:
% show it is realizable on FPGA
%For paths we don't find:
% what does cadence say?
%For unrealizable paths:
% Can we confirm results with Cadence?
\section{Related Work}
%knox
%defines a new variant of refinement: information preserving refinement although
%difference btwn this and refinement is unclear.
%Ruling out side
%channels is different than fully understanding how information
%%ows. User must write the specification (correctly -- this defines
%correctness), refinement relation, physical implementation (of course -- .v
%file), driver, hints to the symbolic execution, emulator, and proof
%script. Functional specification and driver are trusted. Implementation is the
%thing to verify. Hints, Relation, Emulator, and Proof Script are the proof
%artifacts and verified by the framework, but are difficult to get right, i.e., a
%failed verification doesn't help the developer fix these proof artifacts to get
%ti right. Our tool
%could help. A different use-case (smaller, well specified designs like HSMs) and
%therefore different requirements and goals. Still, we expect our tool could help
%designers make use of a tool like Knox, providing information that informs the
%formal specification, refinement relation, and proof script that a designer must
%write to use Knox.
%Use of guided symbolic execution: Uses symbolic execution in a model-checking
%sort of way, but this part is unclear. Uses Rosette and Racket. Human provides
%hints to when states can be concretized, path condition can be weakened, terms
%can be rewritten, terms can be replaced with a fresh variable
%(over-approximate), etc. to manage the search space explosion.
%upec
%Unique Program Execution Checking (UPEC) is a formal method to detect
%vulnerabilities to covert channels in a hardware design, and can find transient
%execution
%attacks~\cite{fadiheh2023exhaustive}. However, much
%of the approach is manual, involving writing a list of constraints. Our tool can
%complement this approach by using analysis of the hyperflow graph to generate
%constraints. UPEC also has broader applications in in detecting functional
%design bugs which cause confidentiality violations~\cite{muller2021formal}.
%From the UPEC thesis~\cite{mohammad2022unique}:
%UPEC is primarily about how to formulate properties? The properties are then
%checked using Interval Property Checking. Interval Properties -- a class of
%properties that can be stated as an implication in which the antecedent and
%consequent are described over a finite time interval. These are proven using
%proof by induction (why aren't these just called inductive
%properties?? nm, slightly different. not a base case and inductive step, rather
%an implication that is proven to hold over an overapprox of the design). Starting from a fully symbolic state, and checking that the
%property holds for given time interval, proves the property for the whole
%design. One weakness, is that many true properties may not be provable by this
%%overapproximation method. A CEX, may not be a true counterexample of the design
%starting from a reset state. How to tell the difference?
%\cks{From John's talk: https://software.imdea.org/~ab/Publications/tlad.pdf}
%\cite{Kozyri2022expressing} Monograph (SoK) on Information Flow properties. We can
%refer to this for the textbook definition of our properties. Look at for
%references for information flow definitions, hyperproperties.
\paragraph{\textbf{Symbolic Execution of HW Designs for Information Flow Analysis}}
EISec uses netlist-level
symbolic execution to verify information-flow safety and
quantify confusion and diffusion in cryptographic
modules~\cite{fowze2022eisec}. Our work improves upon EISec by
allowing analysis at the RT-level and enabling verification of a wider class of
information-flow properties. Other tools
use symbolic simulation
(e.g.,~\cite{torlak2014rosette}) %, either in combination with manual
%refinement proofs~\cite{athalye2022knox} or information flow
%tracking~\cite{cherupalli2017software}
to verify particular binaries running on the
hardware~\cite{athalye2022knox,cherupalli2017software}.
%% Work by Cherupalli et al.
%% uses gate-level symbolic simulation in conjunction with software-based information flow tracking flow system to eliminate vulnerabilities in hardware \cite{cherupalli2017software}
%\cite{cherupalli2017software}
%Gate-level symbolic simulation (not SW-style symbolic execution) for finding information flow vulnerabilities in HW/SW -- an IoT processor running the
%particular IoT application. Has comprehensive list
%of references for how information flow analysis (mostly taint tracking, but not
%all) is used to assess security and privacy of systems (mostly
%software). ``symbolic gate-level simulation of the application binary on the
%netlist''. Key information flow policy assessed is memory leakage (tainted to
%untainted output). Evaluation on openMSP430.
\paragraph{\textbf{Symbolic Execution of SW for Information Flow Analysis}}
%\cks{I think all three use self-composition for SE of IF?}
The software community was perhaps the first to leverage symbolic execution to
verify information flow. The approach has been used in combination with taint
tracking~\cite{cha2012mayhem}, to find and mitigate side
channels~\cite{bao2021symbolic,wang2017cached,wang2019identifying,brotzman2019casym},
and to identify programs that are
vulnerable to transient execution attacks~\cite{guarnier2020spectector}.
%% These techniques have also used in the Mayhem engine, which
%% uses taint tracking to guide execution towards vulnerabilities in binaries~\cite{cha2012mayhem}, as well as in CacheD to discover cache-based timing side channels in production software~\cite{wang2017cached,wang2019identifying}. Spectector~\cite{guarnier2020spectector} uses the symbolic execution to analyze
%% the flow of information in software. Their goal is to find programs that leak information under
%% a speculative execution model. Our work carries similar ideas into the hardware domain.
%% CaSym is a cache-aware software symbolic execution engine for side channel detection and mitigation \cite{brotzman2019casym}.
\paragraph{\textbf{Symbolic Execution of SW or HW to Find Exploitable Flaws}}
There is a long history of using symbolic execution in software to find
exploitable security flaws
(e.g,~\cite{avgerinos2011automatic,avgerinos2014automatic,renzelmann2012symdrive}).
In hardware, symbolic execution has been used to find violations of and exploits
for security-critical assertions~\cite{zhang2018end} and to find and trigger
trojans in the Verilog RTL~\cite{Shen2018SymbolicEB}. As
with SEIF, the main challenge is guiding search through the tree to find the
salient paths.
%% Work on Automatic Exploit Generation~\cite{avgerinos2011automatic,avgerinos2014automatic} has explored preconditioned symbolic execution, which restricts exploration to only likely-exploitable regions of the state space.
%% Our technique shares ideas/philosophy with preconditioned symbolic execution. In
%% PSE, the input space is limited to prune the search tree. In contrast, we add constraints that allow continued information flow, which guides the search through the tree.
%% SymDrive~\cite{renzelmann2012symdrive} is a tool which uses symbolic execution to find bugs in software drivers and allows developers to guide symbolic execution down particular paths. Coppelia~\cite{zhang2018end} describes a technique for performing backwards symbolic execution to find security violations and generate exploits for hardware. There has also been work using symbolic execution to generate test cases to trigger trojans in Verilog RTL \cite{Shen2018SymbolicEB}.
\paragraph{\textbf{Information Flow Tracking in HW}}
The state of the art for information flow analysis in hardware is information flow
tracking (IFT), which
instruments a design with tracking logic~\cite{tiwari2009complete}. Many tools
operate at the netlist level, although some operate at
the RTL level~\cite{ardeshiricham2017register}. IFT has also been used in analog
designs~\cite{bidmeshki2017information}, and tools exist to synthesize
designs that incorporate
tracking logic~\cite{pilato2018tainthls,pieper2020dynamic}.
IFT can be used to check
hyperproperties and has been used to verify the safety and security of many different systems~\cite{clarkson2010hyperproperties,Kozyri2022expressing}\cite{tiwari2009execution,boraten2018securing}\cite{meza2022safety}\cite{restuccia2022framework,restuccia2021aker}\cite{ardeshiricham2017clepsydra}
\cite{hu2016detecting}\cite{jin2012proof}. IFT has also been
used to automatically generate information flow properties for use with formal
verification engines~\cite{Deutschbein2021Isadora,Deutschbein2022JCEN}. We used
these properties in our evaluation.
%and has been used to
%enforce non-interference~\cite{tiwari2009execution,boraten2018securing},
%verify safety of communication protocols~\cite{meza2022safety}, reason about
%access control violations~\cite{restuccia2022framework,restuccia2021aker},
%detect timing flows in hardware~\cite{ardeshiricham2017clepsydra}, find hardware
%trojans~\cite{hu2016detecting}, and to
%ensure data secrecy and hardware trust~\cite{jin2012proof}.
%% \cks{Kaki, any chance we use
%% any of these properties in our analysis? If so, I'd change the last sentence
%% to say that.}
\paragraph{\textbf{Formal Analysis for Information Flow}}
Proof-checking approaches have been used for detecting
security vulnerabilities in hardware designs \cite{fadiheh2023exhaustive} \cite{kong2017using}.
These approaches are often less automated, more time
intensive, and tackle smaller designs, for stronger results that are both sound and complete.
VeriCoq translated Verilog to Coq for proof-carrying designs \cite{bidmeshki2015vericoq}. Another approach is
to use self-composition, or program products, to verify information-flow properties~\cite{eilers2021product}.
Security extensions in the hardware description language can enforce
information flow policies at the language level~\cite{ferraiuolo2017secverilog, deng2017secchisel, li2011caisson, li2014sapper,zhang2015secverilog, ardeshiricham2019verisketch}.
%Full, formal verification of information flow is fundamentally different than
%the SEIF approach and makes different trade-offs. These approaches are often less automated, more time
%intensive, and tackle smaller designs, for stronger results that are both
%sound and complete.
%These platforms require extensive manual
%effort, and SEIF could potentially be used to ease the manual
%burden.
%%Prior work has also formally verified information-flow properties via program products~\cite{eilers2021product}.
%% Leaving out as not quite in scope (and we're short on space)
%% There has also been work on providing architecture support of information flow tagging and labeling, in SAFE!\cite{amorim2014verified} which aims to prove non-interference and an ISA for a RISC-V processor that uses the labels to eliminate or mitigate timing channels \cite{zagieboylo2019using}.
%% malicious flows of information where policy violations can be detected.
%% Specific applications include Clepsydra, which detects timing flows in hardware~\cite{ardeshiricham2017clepsydra}, and flow tracking in analog designs~\cite{bidmeshki2017information}.
%This is mentioned in the intro and I don't know what to do with it here.
%% EXERT is an information flow analysis framework, implemented at the
%% gate-level, that uses SAT solving to produce test benches to trigger trojans
%% and find possible privilege escalation vulnerabilites. \cite{wu2022exert}.
%% GLIFT is a ga
%% te-level framework information flow framework that has been used to find hardware trojans \cite{hu2016detecting}.
%% \subsection{Not Organized Yet}
%% Model Checking for Information Flow (temporal logic for
%% hyperproperties)~\cite{clarkson2014temporal}
%Isadora is a tool which automates generation of hardware information flow properties, by combining flow tracking with specification mining \cite{Deutschbein2021Isadora,Deutschbein2022JCEN}. This provides a complementary lens through which to view our work. Properties of interest generated by Isadora can be used to focus our analysis on interesting parts of the hyperflow graph, while our tool can highlight specific flows and counter-examples to properties Isadora discovers.
%Assertion verification for confidentiality in HW~\cite{kong2017using}. \cks{Need
% to read -- not sure if that is an accurate representation} \kar{i put it in the first section, i think it's proof checking?, seems similar to UPEC}
%Non-interference for NOCs~\cite{boraten2018securing}. \cks{Read for designs and
% properties. Looks at NOCs.}
%A key contribution of spectector is the definition of speculative
%non-interference. Spectector uses symbolic execution of SW to find programs that
%violate this notion of non-interference -- programs for which speculatively executed (and
%mispredicted) branches in the CPU core can lead to information flow to the
%attacker that would not flow to the attacker in the absence of speculative
%execution. Spectector uses symbolic execution to analyze the flow of
%information (in SW, rather than in HW), but has some key differences. First, the
%goal is different, Spectector is looking for SW programs that can leak
%information under a speculative execution model, but not otherwise; our work is
%looking for (or proving the absence of) particular flows of information within a
%hardware design from a source signal to a sink signal or port. In many ways the
%methodology is similar; both use symbolic execution to build descriptions of
%information flow through the design (or program). Spectector compares flows in both speculative and non-speculative
%execution models and uses an SMT solver to compare the two cases; this work
%assesses individual flows that follow a particular path and uses an SMT solver
%to find corresponding test-cases.
%Learch paper~\cite{?} HW verification w/NN~\cite{?}. Recent work is using ML and
%in particular NN to guide symbolic execution of hardware designs and to build
%test-cases for use with simulation-based verification engines. Neither are in
%the context of information flow. It is possible to define features and coverage
%metrics from the IFG-guided symbolic execution engine and leverage these deep
%learning techniques.
%\cks{moved from elsewhere}
%A non-interference property is a hyperproperty, and is typically stated as a
%2-safety property: \cks{write out
% property}~\cite{clarkson2010hyperproperties,Kozyri2022expressing}.
%\kar{i'm commenting this out b/c i don't think we need it in the related work}
%Model
%checking approaches the problem by stating it as a 2-safety problem and using
%self-composition to verify the property. \cks{flesh this out a bit.} Model
%checking can prove non-interference in some cases~\cite{sthg} and demonstrate
%non-interference up to a bounded number of clock cycles in other
%cases~\cite{sthg}. An alternative approach is to use information flow tracking~\cite{denning}. Input
%signals of interest are labeled with their security level or intended use and a
%flow relation defining how labels propagate through the system is
%defined. Gate-level~\cite{GLIFT} and RTL level information flow tracking~\cite{sthg} adds tracking logic
%to a design, and at the end of execution (or simulation), one can inspect the
%labels of the output signals to determine whether information has flown from a
%labeled input to an output. Information flow tracking can find flows of
%information quickly, even over many clock cycles, but it is a dynamic analysis
%technique and can only find information flows for the particular traces seen
%during simulation. Information flow tracking can also fail to take into account
%semantic notions of flow leading to false positive reports of influence from $x$
%to $y$ where there are none. See section~\ref{sec:sthg} for further discussion
%of this issue.
% i am commented this out because i think we address it else where?
%\cks{How do the flows we identify compare to those of gate-level taint
% tracking~\cite{}, non-interference~\cite{goguen1982}, observational non-interference~\cite{}?
%I think we can provide enforcement of observational non-interference and be more
%precise in our enforcement (fewer false positives)
%than gate-level taint tracking. Gate level taint-tracking will not detect the
%reconvergent no-flow (we will), will not detect the $y <= x XOR x$~\cite{oberg2010theoretical,hu2011theoretical} no-flow, we
%will, will not detect the $if (x XOR x)$ no flow, and neither do we.}
\section{Conclusion}
SEIF combines static analysis and symbolic execution to find
information flows in hardware designs. SEIF improves over static analysis,
eliminating false-positive flows, and finding replayable designs through the
path for true flows. In our experiments, SEIF accounts for 86--90\% of
statically identified flows in three open-source designs. SEIF also leverages
static analysis to explore the designs for 10-12 clock cycles in 4-6 seconds on average.
Additionally, SEIF can be used to find multiple violating paths for security
properties, providing a new angle for security verification.
\section{Acknowledgments}
This material is based upon work supported
by the National Science Foundation under Grant No. CNS-2247754, and by a Meta Security Research Award.
\begin{thebibliography}{10}
\bibitem{eilers2021product}Eilers, M., Meier, S. \& Müller, P. Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security. {\em Computer Aided Verification (CAV)}. (2021)
\bibitem{tiwari2009complete}Tiwari, M., Wassel, H., Mazloom, B., Mysore, S., Chong, F. \& Sherwood, T. Complete information flow tracking from the gates up. {\em Proceedings Of The 14th International Conference On Architectural Support For Programming Languages And Operating Systems}. pp. 109-120 (2009)
\bibitem{tiwari2009execution}Tiwari, M., Li, X., Wassel, H., Chong, F. \& Sherwood, T. Execution leases: A hardware-supported mechanism for enforcing strong non-interference. {\em Proceedings Of The 42nd Annual IEEE/ACM International Symposium On Microarchitecture}. pp. 493-504 (2009)
\bibitem{jin2012proof}Jin, Y. \& Makris, Y. Proof carrying-based information flow tracking for data secrecy protection and hardware trust. {\em 2012 IEEE 30th VLSI Test Symposium (VTS)}. pp. 252-257 (2012)
\bibitem{li2011caisson}Li, X., Tiwari, M., Oberg, J., Kashyap, V., Chong, F., Sherwood, T. \& Hardekopf, B. Caisson: A Hardware Description Language for Secure Information Flow. {\em Proceedings Of The 32Nd ACM SIGPLAN Conference On Programming Language Design And Implementation}. pp. 109-120 (2011), http://doi.acm.org/10.1145/1993498.1993512
\bibitem{li2014sapper}Li, X., Kashyap, V., Oberg, J., Tiwari, M., Rajarathinam, V., Kastner, R., Sherwood, T., Hardekopf, B. \& Chong, F. Sapper: A Language for Hardware-level Security Policy Enforcement. {\em Proceedings Of The 19th International Conference On Architectural Support For Programming Languages And Operating Systems}. pp. 97-112 (2014), http://doi.acm.org/10.1145/2541940.2541947
\bibitem{zhang2015secverilog}Zhang, D., Wang, Y., Suh, G. \& Myers, A. A Hardware Design Language for Timing-Sensitive Information-Flow Security. {\em Proceedings Of The Twentieth International Conference On Architectural Support For Programming Languages And Operating Systems}. pp. 503-516 (2015), http://doi.acm.org/10.1145/2694344.2694372
\bibitem{bidmeshki2015vericoq}Bidmeshki, M. \& Makris, Y. VeriCoq: A Verilog-to-Coq converter for proof-carrying hardware automation. {\em 2015 IEEE International Symposium On Circuits And Systems (ISCAS)}. pp. 29-32 (2015)
\bibitem{hu2016detecting}Hu, W., Mao, B., Oberg, J. \& Kastner, R. Detecting hardware trojans with gate-level information-flow tracking. {\em Computer}. \textbf{49}, 44-52 (2016)
\bibitem{kong2017using}Kong, S., Shen, Y. \& Zhou, H. Using security invariant to verify confidentiality in hardware design. {\em Proceedings Of The On Great Lakes Symposium On VLSI 2017}. pp. 487-490 (2017)
\bibitem{ardeshiricham2017register}Ardeshiricham, A., Hu, W., Marxen, J. \& Kastner, R. Register transfer level information flow tracking for provably secure hardware design. {\em Proceedings Of The Conference On Design, Automation \& Test In Europe (DATE)}. pp. 1695-1700 (2017), http://dl.acm.org/citation.cfm?id=3130379.3130775
\bibitem{ardeshiricham2017clepsydra}Ardeshiricham, A., Hu, W. \& Kastner, R. Clepsydra: Modeling timing flows in hardware designs. {\em 2017 IEEE/ACM International Conference On Computer-Aided Design (ICCAD)}. pp. 147-154 (2017)
\bibitem{deng2017secchisel}Deng, S., Gümüşoğlu, D., Xiong, W., Gener, Y., Demir, O. \& Szefer, J. SecChisel: language and tool for practical and scalable security verification of security-aware hardware architectures. {\em Cryptology EPrint Archive}. (2017)
\bibitem{bidmeshki2017information}Bidmeshki, M., Antonopoulos, A. \& Makris, Y. Information flow tracking in analog/mixed-signal designs through proof-carrying hardware IP. {\em Design, Automation \& Test In Europe Conference \& Exhibition (DATE), 2017}. pp. 1703-1708 (2017)
\bibitem{boraten2018securing}Boraten, T. \& Kodi, A. Securing NoCs against timing attacks with non-interference based adaptive routing. {\em 2018 Twelfth IEEE/ACM International Symposium On Networks-on-Chip (NOCS)}. pp. 1-8 (2018)
\bibitem{pilato2018tainthls}Pilato, C., Wu, K., Garg, S., Karri, R. \& Regazzoni, F. Tainthls: High-level synthesis for dynamic information flow tracking. {\em IEEE Transactions On Computer-Aided Design Of Integrated Circuits And Systems}. \textbf{38}, 798-808 (2018)
\bibitem{zagieboylo2019using}Zagieboylo, D., Suh, G. \& Myers, A. Using information flow to design an ISA that controls timing channels. {\em 2019 IEEE 32nd Computer Security Foundations Symposium (CSF)}. pp. 272-27215 (2019)
\bibitem{pieper2020dynamic}Pieper, P., Herdt, V., Große, D. \& Drechsler, R. Dynamic information flow tracking for embedded binaries using SystemC-based virtual prototypes. {\em 2020 57th ACM/IEEE Design Automation Conference (DAC)}. pp. 1-6 (2020)
\bibitem{restuccia2021aker}Restuccia, F., Meza, A. \& Kastner, R. AKER: A design and verification framework for safe and secure soc access control. {\em IEEE/ACM International Conference On Computer Aided Design (ICCAD)}. (2021), https://par.nsf.gov/servlets/purl/10298115
\bibitem{restuccia2022framework}Restuccia, F., Meza, A., Kastner, R. \& Oberg, J. A Framework for Design, Verification, and Management of SoC Access Control Systems. {\em IEEE Transactions On Computers}. (2022), https://kastner.ucsd.edu/wp-content/uploads/2022/10/admin/tcomputer-aker22.pdf
\bibitem{cherupalli2017software}Cherupalli, H., Duwe, H., Ye, W., Kumar, R. \& Sartori, J. Software-based gate-level information flow security for IoT systems. {\em 50th IEEE/ACM International Symposium On Microarchitecture}. (2017), https://dl.acm.org/doi/pdf/10.1145/3123939.3123955
\bibitem{fadiheh2023exhaustive}Fadiheh, M., Wezel, A., Muller, J., Bormann, J., Ray, S., Fung, J., Mitra, S., Stoffel, D. \& Kunz, W. An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors. {\em IEEE Transactions On Computers}. \textbf{72}, 222-235 (2023,1)
\bibitem{wu2022exert}Wu, J., Fowze, F. \& Forte, D. EXERT: EXhaustive Integrity Analysis for Information Flow Security. {\em Asian Hardware Oriented Security And Trust Symposium (AsianHOST)}. (2022), https://dforte.ece.ufl.edu/wp-content/uploads/sites/65/2022/09/EXERT%5C_AsianHost.pdf
\bibitem{athalye2022knox}Athalye, A., Kaashoek, M. \& Zeldovich, N. Verifying Hardware Security Modules with Information-Preserving Refinement. {\em OSDI}. (2022)
\bibitem{fowze2022eisec}Fowze, F., Choudhury, M. \& Forte, D. EISec: Exhaustive Information Flow Security of Hardware Intellectual Property Utilizing Symbolic Execution. {\em Asian Hardware Oriented Security And Trust Symposium (AsianHOST)}. (2022)
\bibitem{athalye2019notary}Athalye, A., Belay, A., Kaashoek, M., Morris, R. \& Zeldovich, N. Notary: A Device for Secure Transaction Approval. {\em 27th Symposium On Operating Systems Principles (SOSP)}. (2019), https://doi.org/10.1145/3341301.3359661
\bibitem{meza2023hyperflowgraph}Meza, A. \& Kastner, R. Information Flow Coverage Metrics for Hardware Security Verification. (2023), arXiv 2304.08263
\bibitem{ryan2023countering}Ryan, K. \& Sturton, C. Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs. (2023), arXiv 2304.05445
\bibitem{dorsey2020intel}Dorsey, V. \& Morhardt, C. Intel Security Development Lifecycle. (Intel,2020)
\bibitem{he2015model}He, S., Roe, N., Wood, E., Nachtigal, N. \& Helms, J. Model of the Product Development Lifecycle. (Sandia National Laboratories,2015)
\bibitem{YangSP2016}Yang, K., Hicks, M., Dong, Q., Austin, T. \& Sylvester, D. A2: Analog Malicious Hardware. {\em 2016 IEEE Symposium On Security And Privacy (SP)}. pp. 18-37 (2016)
\bibitem{or1200}. OpenRISC 1200 Implementation. , https://github.com/openrisc/or1200
\bibitem{msp430}. openMSP430. , https://opencores.org/projects/openmsp430
\bibitem{farzana2019soc}Farzana, N., Rahman, F., Tehranipoor, M. \& Farahmandi, F. SoC Security Verification using Property Checking. {\em 2019 IEEE International Test Conference (ITC)}. pp. 1-10 (2019)
\bibitem{TrustHub2}Farzana, N., Farahmandi, F. \& Tehranipoor, M. SoC Security Properties and Rules. {\em IACR Cryptol. EPrint Arch.}. \textbf{2021} pp. 1014 (2021)
\bibitem{hicks2015specs}Hicks, M., Sturton, C., King, S. \& Smith, J. SPECS: A Lightweight Runtime Mechanism for Protecting Software from Security-Critical Processor Bugs. {\em ASPLOS}. pp. 517-529 (2015)
\bibitem{bilzor2011security}Bilzor, M., Huffmire, T., Irvine, C. \& Levin, T. Security Checkers: Detecting processor malicious inclusions at runtime. {\em HOST}. (2011)
\bibitem{zhang2017scifinder}Zhang, R., Stanley, N., Griggs, C., Chi, A. \& Sturton, C. Identifying Security Critical Properties for the Dynamic Verification of a Processor. {\em ASPLOS}. pp. 541-554 (2017)
\bibitem{zhang2020transys}Zhang, R. \& Sturton, C. Transys: Leveraging Common Security Properties Across Hardware Designs. {\em Proceedings Of The Symposium On Security And Privacy (S\&P)}. (2020)
\bibitem{trippel2020ICAS}Trippel, T., Shin, K., Bush, K. \& Hicks, M. ICAS: an Extensible Framework for Estimating the Susceptibility of IC Layouts to Additive Trojans. {\em 2020 IEEE Symposium On Security And Privacy (SP)}. pp. 1742-1759 (2020)
\bibitem{Deutschbein2022JCEN}Deutschbein, C., Meza, A., Restuccia, F., Kastner, R. \& Sturton, C. Isadora: Automated Information Flow Property Generation for Hardware Security Verification. {\em Journal Of Cryptographic Engineering (JCEN)}. (2022)
\bibitem{zhang2021sidechannel}Zhang, T., Park, J., Tehranipoor, M. \& Farahmandi, F. PSC-TG: RTL Power Side-Channel Leakage Assessment with Test Pattern Generation. {\em 2021 58th ACM/IEEE Design Automation Conference (DAC)}. pp. 709-714 (2021)
\bibitem{torlak2014rosette}Torlak, E. \& Bodik, R. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. {\em Proceedings Of The 35th ACM SIGPLAN Conference On Programming Language Design And Implementation}. pp. 530-541 (2014), https://doi.org/10.1145/2594291.2594340
\bibitem{cha2012mayhem}Cha, S., Avgerinos, T., Rebert, A. \& Brumley, D. Unleashing Mayhem on Binary Code. {\em Proceedings Of The 2012 IEEE Symposium On Security And Privacy}. pp. 380-394 (2012)
\bibitem{bao2021symbolic}Bao, Q., Wang, Z., Li, X., Larus, J. \& Wu, D. Abacus: Precise side-channel analysis. {\em International Conference On Software Engineering (ICSE)}. pp. 797-809 (2021)
\bibitem{wang2017cached}Wang, S., Wang, P., Liu, X., Zhang, D. \& Wu, D. CacheD: Identifying cache-based timing channels in production software. {\em USENIX Security Symposium}. pp. 235-252 (2017)
\bibitem{wang2019identifying}Wang, S., Bao, Y., Liu, X., Wang, P., Zhang, D. \& Wu, D. Identifying Cache-Based Side Channels through Secret-Augmented Abstract Interpretation. {\em 28th USENIX Security Symposium (USENIX Security 19)}. pp. 657-674 (2019,8), https://www.usenix.org/conference/usenixsecurity19/presentation/wang-shuai
\bibitem{brotzman2019casym}Brotzman, R., Liu, S., Zhang, D., Tan, G. \& Kandemir, M. Casym: Cache aware symbolic execution for side channel detection and mitigation. {\em Symposium On Security And Privacy (SP)}. (2019)
\bibitem{guarnier2020spectector}Guarnieri, M., Köpf, B., Morales, J., Reineke, J. \& Sánchez, A. Spectector: Principled Detection of Speculative Information Flows. {\em 2020 IEEE Symposium On Security And Privacy (SP)}. pp. 1-19 (2020)
\bibitem{avgerinos2014automatic}Avgerinos, T., Cha, S., Rebert, A., Schwartz, E., Woo, M. \& Brumley, D. Automatic exploit generation. {\em Communications Of The ACM}. \textbf{57}, 74-84 (2014)
\bibitem{avgerinos2011automatic}Avgerinos, T., Hao, B. \& Brumley, D. Automatic exploit generation. {\em Network And Distributed System Security Symposium (NDSS)}. (2011)
\bibitem{renzelmann2012symdrive}Renzelmann, M., Kadav, A. \& Swift, M. SymDrive: Testing Drivers without Devices. {\em 10th USENIX Symposium On Operating Systems Design And Implementation}. (2012), https://www.usenix.org/conference/osdi12/technical-sessions/presentation/renzelmann
\bibitem{zhang2018end}Zhang, R., Deutschbein, C., Huang, P. \& Sturton, C. End-to-End Automated Exploit Generation for Validating the Security of Processor Designs. {\em Proceedings Of The International Symposium On Microarchitecture (MICRO)}. (2018)
\bibitem{Shen2018SymbolicEB}Shen, L., Mu, D., Cao, G., Qin, M., Blackstone, J. \& Kastner, R. Symbolic execution based test-patterns generation algorithm for hardware Trojan detection. {\em Comput. Secur.}. \textbf{78} pp. 267-280 (2018)
\bibitem{clarkson2010hyperproperties}Clarkson, M. \& Schneider, F. Hyperproperties. {\em J. Comput. Secur.}. \textbf{18}, 1157-1210 (2010,9), http://dl.acm.org/citation.cfm?id=1891823.1891830
\bibitem{Kozyri2022expressing}Kozyri, E., Chong, S. \& Myers, A. Expressing Information Flow Properties. {\em Foundations And Trends® In Privacy And Security}. \textbf{3}, 1-102 (2022), http://dx.doi.org/10.1561/3300000008
\bibitem{meza2022safety}Meza, A., Restuccia, F., Kastner, R. \& Oberg, J. Safety verification of third-party hardware modules via information flow tracking. {\em 1st Real-Time Intelligent Edge Computing Workshop (RAGE)}. (2022), https://kastner.ucsd.edu/wp-content/uploads/2022/08/admin/rage22-safety.pdf
\bibitem{Deutschbein2021Isadora}Deutschbein, C., Meza, A., Restuccia, F., Kastner, R. \& Sturton, C. Isadora: Automated Information Flow Property Generation for Hardware Designs. {\em Proceedings Of The Workshop On Attacks And Solutions In Hardware Security (ASHES)}. (2021)
\bibitem{ferraiuolo2017secverilog}Ferraiuolo, A., Xu, R., Zhang, D., Myers, A. \& Suh, G. Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis. {\em Proceedings Of The Twenty-Second International Conference On Architectural Support For Programming Languages And Operating Systems}. pp. 555-568 (2017), http://doi.acm.org/10.1145/3037697.3037739
\bibitem{ardeshiricham2019verisketch}Ardeshiricham, A., Takashima, Y., Gao, S. \& Kastner, R. VeriSketch: Synthesizing Secure Hardware Designs with Timing-Sensitive Information Flow Properties. {\em Proceedings Of The 2019 ACM SIGSAC Conference On Computer And Communications Security}. pp. 1623-1638 (2019)
\end{thebibliography}
\section{Appendix}
\subsection{Determining the Stall Bound}
We empirically determined the number of clock cycles to stall for each heuristic that involved stalling: baseline 1,
bounded stalling with backtracking and the UNSAT core heuristic. Once we do not see any significant gains from
stalling for an additional clock cycle, we have found our bound. The results for each of the three heuristics
are shown in Figures \ref{fig:baseline1-graph-a}, \ref{fig:bd-stalling-graph-a}, and \ref{fig:stalling-unsat-graph-a}.
\begin{figure}[h]
\centering
\includegraphics[width=\columnwidth,trim = 0 20 0 55,clip]{figures/baseline1-stalling-graph.png}
\caption{Empirically determining the stall
bound for baseline 1.}
\label{fig:baseline1-graph-a}
\end{figure}
\begin{figure}[h]
\centering
% \includegraphics[scale = 0.45]{figures/bd-stalling-graph.png}
\includegraphics[width=\columnwidth,trim = 0 20 0 65,clip]{figures/bd-stalling-graph.png}
\caption{Empirically determining the stall
bound for bounded stalling with backtracking.}
\label{fig:bd-stalling-graph-a}
\end{figure}
\begin{figure}[h]
\centering
% \includegraphics[scale = 0.45]{figures/bd-stalling-graph.png}
\includegraphics[width=\columnwidth,trim = 0 20 0 65,clip]{figures/stalling-unsat-graph.png}
\caption{Empirically determining the stall
bound for stalling with the UNSAT core heuristic.}
\label{fig:stalling-unsat-graph-a}
\end{figure}