=Paper=
{{Paper
|id=Vol-3087/paper_9
|storemode=property
|title=EnnCore: End-to-End Conceptual Guarding of Neural Architectures
|pdfUrl=https://ceur-ws.org/Vol-3087/paper_9.pdf
|volume=Vol-3087
|authors=Edoardo Manino,Danilo Carvalho,Yi Dong,Julia Rozanova,Xidan Song,Mustafa Mustafa,Andre Freitas,Gavin Brown,Mikel Luján,Xiaowei Huang,Lucas Cordeiro,Bertrand Braunschweig,Rodolphe Gelin,François Terrier
|dblpUrl=https://dblp.org/rec/conf/aaai/ManinoCDRSMFBL022
}}
==EnnCore: End-to-End Conceptual Guarding of Neural Architectures==
https://ceur-ws.org/Vol-3087/paper_9.pdf
EnnCore: End-to-End Conceptual Guarding of Neural Architectures
Edoardo Manino, 1 Danilo Carvalho, 1 Yi Dong, 2 Julia Rozanova, 1 Xidan Song, 1 Mustafa A.
Mustafa, 1,3 Andre Freitas, 1,4 Gavin Brown, 1 Mikel Luján, 1 Xiaowei Huang, 2 Lucas Cordeiro 1
1
Department of Computer Science, The University of Manchester, Manchester, M13 9PL, U.K.
2
Department of Computer Science, University of Liverpool, Liverpool, L69 3BX, U.K.
3
imec-COSIC, KU Leuven, Leuven-Heverlee, B-3001, Belgium
4
Idiap Research Institute, Martigny, 1920, Switzerland
{lucas.cordeiro, andres.freitas, mustafa.mustafa}@manchester.ac.uk, {yi.dong, xiaowei}@liverpool.ac.uk
Abstract According to a recent survey on the state-of-the-art of
verification and synthesis methods for cyber-physical sys-
The EnnCore project addresses the fundamental security tems (Cordeiro, de Lima Filho, and Bessa 2020), most pa-
problem of guaranteeing safety, transparency, and robustness
pers published in the area in the past ten years only study the
in neural-based architectures. Specifically, EnnCore aims at
enabling system designers to specify essential conceptual/be- verification of safety properties over mathematical represen-
havioral properties of neural-based systems, verify them, and tations of DNNs. However, a top-to-bottom verification pro-
thus safeguard the system against unpredictable behavior and cess of DNNs will need to cover various aspects, including,
attacks. In this respect, EnnCore will pioneer the dialogue be- for example, the external phenomena with which the DNN
tween contemporary explainable neural models and full-stack models interact and evolve. Thus, there is a considerable gap
neural software verification. This paper describes existing between low- and high-level models and between engineer-
studies’ limitations, our research objectives, current achieve- ing and theoretical research efforts.
ments, and future trends towards this goal. In particular, we The EnnCore project1 , which stands for “End-to-End
describe the development and evaluation of new methods, al-
gorithms, and tools to achieve fully-verifiable intelligent sys-
Conceptual Guarding of Neural Architectures”, aims to fill
tems, which are explainable, whose correct behavior is guar- this gap. It has ambitious cross-cutting and far-reaching
anteed, and robust against attacks. We also describe how En- goals to provide a coherent and self-containing framework
nCore will be validated on two diverse and high-impact ap- for specifying a conceptual safeguard core to neural-based
plication scenarios: securing an AI system for (i) cancer di- (NB) Artificial Intelligence (AI) systems and verifying their
agnosis and (ii) energy demand response. actual implementations considering security aspects. Our
setting draws on all of the above aspects: it covers the full
range, from engineering details to abstraction and verifica-
1 Introduction tion, and reasoning and explainability about model evolution
Deep neural networks (DNNs) are computing models typi- and learning.
cally deployed for classification, decision-making, and pat- As a result, EnnCore addresses a fundamental research
tern recognition problems (Bishop 2006). Recently, various problem to ensure the security of neural-enabled compo-
safety-critical tasks deployed DNNs, e.g., Covid-19 diagno- nents by taking into account their entire lifecycle from de-
sis (Nour, Cömert, and Polat 2020) and steering control in velopment to deployment. Solving this problem has a far-
self-driving cars (Wu et al. 2021). In these contexts, how- reaching impact on areas such as health and energy, which
ever, incorrect classifications can cause severe damages. It heavily depend on secure and trusted software components
is well-known in the literature that adversarial disturbances to meet safety-critical requirements. Hence, our overall re-
can make DNNs misclassify objects, thus causing severe search objective is to have a long-term impact on writ-
damage to users of safety-critical systems. For example, ing secure and trusted AI-based software components, thus
Eykholt et al. (Eykholt et al. 2018) described that noise and contributing to a shared vision of fully-verifiable software,
disturbances, such as graffiti on traffic signals, could result where underlying neural-based architectures are built with
in target misclassification during operation. Moreover, as strong symbolic and mathematical guarantees.
DNNs are difficult to interpret and debug, the whole scenario To achieve this objective, EnnCore will design and vali-
becomes even more problematic (Lundberg and Lee 2017). date a full-stack symbolic safeguarding system for NB ar-
Hence, there is a need for techniques to assess their struc- chitectures. It will advance the state-of-the-art in the devel-
tures and verify their results and behavior. Consequently, opment of secure DNN models by mapping, using, and ex-
there is a growing interest in verification and interpretability tending explainability properties of existing neuro-symbolic
methods for ensuring and explaining safety, accuracy, and DNN architectures (e.g., Graph Networks, Differentiable In-
robustness for DNNs. ductive Logic Programming), thus safeguarding them with
Copyright © 2022 for this paper by its authors. Use permitted under symbolic verification, abstract interpretation, and program
Creative Commons License Attribution 4.0 International (CC BY
1
4.0). https://enncore.github.io/
research areas to tackle the safety and security of NB ar-
chitectures. Finally, we conclude and describe future work
in Section 6.
2 Limitations of Existing Work
Explainable/Interpretable ML models. Doshi-Velez and
Kim (Doshi-Velez and Kim 2017) define interpretability
as “the ability to explain or to present in understandable
terms to a human”. Interpretability is an active area of ma-
chine learning. The recent Neuro-Symbolic (NS) architec-
tures (Garcez et al. 2019) inherit the strengths of deep learn-
ing models, while extending it with explainability and fine-
grained/abstractive reasoning capabilities. NS models such
as Graph Networks (GNs) (Alshahrani et al. 2017) and Dif-
ferentiable ILP (Manhaeve et al. 2018) operate over and de-
Figure 1: EnnCore methodology. pend upon knowledge bases and focus on addressing infer-
ence problems which require relational reasoning and com-
binatorial generalization. No prior work has exploited: (i)
synthesis methods. EnnCore will pioneer the interdisci- the use of knowledge-based neuro-symbolic architectures
plinary dialogue between explainable AI and formal veri- for supporting end-users communicating their security con-
fication. In particular, it will deliver safeguarding for NB ar- straints and (ii) the combination of explainability with sym-
chitectures with the following properties: bolic verification to assure security properties.
1. Full-stack symbolic software verification: EnnCore will Verification of DNN Models. Verification of DNN models
develop the first bit-precise and scalable symbolic ver- has attracted lots of attention recently, including unique ap-
ification framework to reason over implementations of proaches from formal verification (Huang et al. 2017; Katz
DNNs, thereby providing additional guarantees of secu- et al. 2017; Lomuscio and Maganti 2017; Wu et al. 2020),
rity properties concerning the underlying hardware. We which deals with the problem through exhaustive search,
will exploit state-of-the-art abstract interpretation and SMT constraint solving, MILP constraint solving, and re-
synthesis techniques to synthesize invariants to prune the duction to two-player game, respectively. A key problem re-
state-space exploration and thus verify intricate security mains on the scalability – the theoretical complexity of the
properties to ensure confidentiality, integrity, and avail- verification problem is NP-complete either on the number of
ability. hidden neurons (Katz et al. 2017) or the input dimensions
(Ruan, Huang, and Kwiatkowska 2018). This pessimistic
2. Explainability/Interpretability: EnnCore will pioneer the result has led to the consideration of approximation meth-
integration of knowledge-based and neural explainabil- ods, such as abstract interpretation (Gehr et al. 2018), inter-
ity methods to support end-users specifying security con- val analysis (Li et al. 2019), and polynomial approximation
straints and diagnosing security risks in order to provide (Huang et al. 2019). These methods provide soundness guar-
security assurances as NB models evolve. Attention will antees to the result but cannot ensure completeness. Such a
be given to the quantitative and qualitative characteriza- relaxation on the guarantees can improve the scale of the net-
tion of semantic-drift phenomena in security scenarios. work models that the methods can work with but still cannot
3. Scalable: EnnCore will systematically combine contem- reach the industrial-scale network models, even when GPU-
porary symbolic methods for explaining, interpreting and based Parallelisation is applied (Ruan et al. 2019). Besides,
verifying neural representations. In particular, we will they are often restricted by the types of layers or activation
develop a neuro-symbolic safeguard framework by link- functions they can work with.
ing the structural knowledge-based representation ele- The above observation has led to the development of the
ments to the attentional architecture elements to achieve other thread of works called testing methods, which gener-
scalability and precision in an unprecedented manner. ate a large number of test cases to intensively test the exis-
EnnCore will systematically validate the system using two tence of errors, such as (Wicker, Huang, and Kwiatkowska
different case studies from different domains: healthcare and 2018; Sun et al. 2018). Furthermore, the generation of test
energy, in order to achieve fully-verifiable intelligent sys- cases may often be guided by the coverage metrics such
tems that are explainable, ensure behavior correctness and as neuron coverage (Pei et al. 2017) or MC/DC (Sun et al.
are robust against unanticipated behaviors and attacks. 2019). While it is arguable whether the generated test cases
The remainder of the paper is organized as follows. In are representative for the property to be verified, the test-
Section 2, we discuss the related work, including the limi- ing results can be utilized to either understand the internal
tation of existing studies. Section 3 describes a logical basis working mechanism (Huang et al. 2021b) of neural network
for proposing our approach as part of the EnnCore project, models or support safety argument (Zhao et al. 2020a) to-
while Section 4 outlines our research objectives. Section 5 gether with the verification results. Please refer to a recent
describe our current achievements broken down into four survey (Huang et al. 2020), or tutorial (Ruan, Yi, and Huang
2021) for more discussions on the verification and testing
techniques for neural network models.
Verification of Actual Implementations of DNNs. While
existing verification methods work with DNN models
and adversarial examples (i.e., a small perturbation on a
correctly-labeled input leads to a different classification), it
has been pointed out in (Odena et al. 2019) that there are
errors in the Tensorflow graph representation of DNNs, a
lower-level implementation of DNNs, such as numerical er-
rors and disagreements between DNN implementations and
their quantized versions. It is reasonable to believe that,
when working with code-level implementations, e.g., on the
Compute Unified Device Architecture (CUDA) and GPU
hardware, there will be other errors, including security loop-
holes, that are more difficult to detect and mitigate than on
CPU implementations (Miele 2016; Di et al. 2020).
Prior work focused on the verification of the robust-
ness of the neural net with respect to its models (Huang Figure 2: EnnCore holistic approach.
et al. 2017; Katz et al. 2017; Sun et al. 2018; Zheng et al.
2016). In these approaches, off-the-shelf Satisfiability Mod-
ulo Theories (SMT) solvers are used to find robustness vio- decision making for medical diagnosis. For energy, Urban-
lations. However, this verification scheme cannot precisely chain3 requires a fair, explainable, and trusted decision mak-
capture issues that can be introduced in the implementa- ing system to ensure the security and privacy of clients’ data.
tions of DNNs. There exist four reasons: (i) one cannot On the other hand, EnnCore will bridge the gap between
model bit-level operations using the theory of integers and the user’s need to communicate their security constraints,
reals (Cordeiro, Fischer, and Marques-Silva 2011); (ii) li- and the technical challenges involved in formalising these
braries, such as TensorFlow, often take advantage of avail- constraints and checking whether neural-based system sat-
able Graphical Processing Units (GPUs) to explore the in- isfy them. In this respect, we consider explainability/inter-
herent parallelism of DNNs, so the translation to GPUs can pretability techniques as a fertile common ground for trans-
be problematic; (iii) some security vulnerabilities cannot be lating the user’s requirements to rigorous mathematical con-
detected in high-level models since they depend on imple- straints. Furthermore, we believe that exploiting the struc-
mentation aspects (e.g., finite word-length); lastly (iv) there ture of such constraints, and the neural-based architecture
exists no connection between automated verification and ex- that is required to satisfy them, is the key towards a truly
plainability approaches, making it difficult to interrogate a scalable full-stack verification approach.
system if something goes wrong.
Towards this, Pereira et al. (Pereira et al. 2017) propose to
verify CUDA programs written for GPU platforms with an 4 Research Objectives
SMT-based context-bounded checking technique. They de- EnnCore aims to fundamentally shift the state-of-the-art of
veloped ESBMC-GPU, which is the first verifier to discover what is achievable in formal verification of AI-based soft-
adversarial cases and validate coverage methods in DNNs ware systems to make them secure and trusted against unan-
using the cuBLAS and cuDNN libraries (Sena et al. 2019). ticipated behavior and attacks. We are convinced that this
However, Pereira et al. (Pereira et al. 2017) do not exploit cannot be achieved by a “proof-of-concept implementation”
invariant inference to prune the state-space exploration for with an artificial case study. This particular approach will
greater scalability. Also, their approach cannot explain the not have much credibility – and thus impact – with systems
parameters of the DNN implementation to understand the and software engineers. We will work in close collaboration
root cause of errors. with industrial partners to tackle real-world case studies in
healthcare and energy domains. We will also use real data
3 Rationale and Approach and work with domain experts to develop and validate our al-
We believe that a holistic approach is necessary to overcome gorithms, methods and tools. In a multidisciplinary fashion,
the challenges and limitations listed in Section 2. To this EnnCore will link two areas, which include neuro-symbolic
end, EnnCore will pioneer the dialogue between all the very and explainable machine learning and software verification,
different components of the contemporary AI safety stack to deliver a full-stack security mechanism for DNNs operat-
(see Figure 2). ing in safety-critical scenarios. Our core objectives are:
On the one hand, we will draw inspiration and sup- O1: Develop a novel conceptual/symbolic safeguard mech-
port from the diverse industrial experiences of our partners. anism for neuro-symbolic platforms
For healthcare, digital Experimental Cancer Medicine Team
(dECMT)2 requires a provably correct, trusted, explainable Research UK Manchester Institute (https://digitalecmt.org/).
3
Urbanchain develops a world-leading platform for energy gen-
2
dECMT is a clinical digital research group based in the Cancer erators in the wholesale market (https://www.urbanchain.co.uk/).
EnnCore will pioneer the use of neuro-symbolic architec- grid constraints (Dudjak et al. 2021). To complete this effi-
tures and explainability/interpretability mechanisms to sup- ciently and effectively, the supplier needs to predict the half-
port end-users specifying a conceptual safeguard core to hourly electricity consumption of each of their customers.
neural-based AI systems. The project will also contribute to To achieve this, the energy supplier deploys an AI model that
a broad and in-depth systematic analysis of the impact of ex- uses their customers’ historical consumption data to predict
isting explainability/interpretability mechanisms in security their consumption data for the next half-hourly time slot.
scenarios. These mechanisms include the interpretation of Unfortunately, this approach allows the supplier to have ac-
high-dimensional embeddings, attentional mechanisms, de- cess to households’ fine-grained consumption data, which
coding from intermediate representations and black-box de- poses a high risk to users’ privacy (Mustafa, Cleemput, and
bugging methods using artificially generated datasets. Abidin 2016) as well as hinders the adoption of smart me-
O2: Develop scalable SMT theories and invariant infer- ters (Briggs, Fan, and Andras 2020).
ence methods for DNNs Up to now, we have performed security analyses of both
EnnCore will develop new SMT theories to reason about the use cases to identify potential threats to the AI models, hence
safety and security of actual implementations of DNNs. Our specifying concrete security requirements/properties that
ultimate goal is to mitigate security vulnerabilities and in- these AI models should satisfy. Apart from the ‘standard’
correct predictions, which make AI-based applications sus- confidentiality, integrity, and availability requirements, we
ceptible to errors and mischance. Additionally, EnnCore will have identified the following properties relevant to AI mod-
develop a new invariant inference method based on the struc- els: robustness, transparency, auditability (traceability), ac-
ture of the DNNs. We aim to simplify the DNN output com- countability, and privacy.
putation for some input intervals using abstract interpreta- Robustness ensures that AI models are resilient against
tion and program synthesis. In particular, we will exploit in- malicious input and corner cases (a.k.a adversarial exam-
variant inference to prune the state-space exploration for ver- ples). Transparency ensures that all phases of an AI model
ifying security properties in real implementations of DNNs. processing chain (including the technical details of the mod-
O3: Grounding, deploying and evaluating high-impact els and the training data used) are well documented. Au-
real-world use cases ditability (traceability) ensures that all the processing steps
EnnCore will be co-designed with industrial and clinical of the AI models (i.e., cause-effect) can be traced by third
partners around exemplary use-case scenarios. The selected parties if needed. Finally, accountability ensures evidence
use cases reflect standard security requirements for DNNs, of who has developed/managed/maintained every compo-
which are transferable to other sectors such as automotive nent/step of the AI model. These four properties are closely
and consumer electronics. Additionally, usability is at the related to each other and contribute to the explainability of
center of the unique value proposition of EnnCore, where AI models. On the other hand, privacy ensures that sensitive
the model can interface with end-users (system designers user data and sensitive AI models are protected from unau-
and security experts). We will allow users to state areas thorized entities, sometimes even from the companies that
within the model that should be safeguarded. have developed and managed the AI models.
To ensure AI models’ robustness against malfunction and
5 Current Achievements and Future Trends attacks, one promising approach is to adopt robust training
The proposed research is broken down into four research ar- for AI models (Gehr et al. 2018). This ensures that the AI
eas: Real Case-Studies & Integrated Evaluation, Explain- models are already fed with data representing potential cor-
able Neuro-Symbolic Safeguard Framework, Symbolic Ver- ner cases in the training phases. To achieve this, the train-
ification Framework for AI, and Verifying Security in Em- ing data is usually augmented by adding a certain degree
bedded Software running in GPUs. In the following, we de- of randomness. The DiffAI framework (Mirman, Gehr, and
scribe the research contents of each area. In particular, we Vechev 2018) has successfully applied this approach to de-
provide details of what has been achieved to date and what velop AI models that are provably robust. This is achieved
we intend to tackle as future work. by deploying abstract interpretation techniques by overap-
proximating the AI system’s behavior. However, the DiffAI
5.1 Real Case-Studies & Integrated Evaluation framework has been designed to process images. As a next
EnnCore aims to tackle two real-world use cases in two step, we plan to adapt the DiffAI framework to process other
distinct domains: health and energy. In the health domain, types of input data, e.g., biomarkers.
the use case is cancer diagnoses (Lee et al. 2021), where a To ensure that AI systems protect user-sensitive data, de-
medical institution (e.g., hospital) aims to determine if sus- ploying Federated Learning (FL) (Bonawitz et al. 2019) is
pect patients have cancer or not based on analyzing a set of a promising approach. FL, by design, allows end-users to
biomarkers. To achieve this, the medical institution deploys train their models locally, never share their sensitive raw
an AI model that uses the patients’ biomarkers to predict the data, yet benefit from the data of others. This is achieved
likelihood of a patient having (or developing) cancer. In the by sharing only the gradients of the locally trained and de-
energy domain, the use case is demand response (Albadi and ployed AI models, which are then aggregated to build a
El-Saadany 2008), where an energy supplier company aims global model, distributed to the end-users. Although it al-
to match their customers’ energy consumption with the en- ready provides a good level of user privacy protection, this
ergy supply available, in order to facilitate peer-to-peer en- approach has some limitations. For example, the gradients of
ergy trading (Capper et al. 2021) without violations of the the locally trained AI models can reveal information about
the model itself and/or the data used for the local training the design of generative models for natural language infer-
of the models (Melis et al. 2019; De Cristofaro 2021). In ence with better disentanglement of latent factors. While
addition, a single global AI model does not always provide representing the meaning of a sentence or an inference
the best possible outcome for all the end-users. To address step in a continuous latent sentence space, models will aim
these limitations, we plan to deploy advanced cryptographic for specializing latent dimensions to capture consistent lin-
techniques for secure computation (homomorphic encryp- guistic and inference phenomena (e.g., tense variations for
tion and multiparty computation) to perform the gradient ag- verbs), allowing for both interpretability and control. In
gregation and devise the global model in a secure way such (Mercatali and Freitas 2021), we proposed a variational au-
that no entity has access to the gradients provided by the toencoder (VAE) model which better disentangles sentence
individual end-users. In addition, to improve performance, discrete generative language factors. Recent work is expand-
we plan to adopt a clustering method (Sattler, Müller, and ing the same level of linguistic control via disentanglement
Samek 2021), which would classify the end-users based on for abstract sentences and multi-hop inference.
their data into several clusters, creating variants of the global The level of additional control needs to be accompanied
model, which will contribute differently to the final model by methodologies that can measure and qualify the internal
used by each of the individual end-users. Our approach will properties of these embedding spaces. For example, prob-
be tested on the energy use case to predict individual users’ ing or diagnostic classification (Hewitt and Liang 2019; Fer-
household electricity consumption data. reira et al. 2021) is a method for investigating whether a set
of intermediate (e.g., semantic) features are present in la-
5.2 Safeguards for Explainable Neuro-Symbolic tent spaces. In EnnCore, we extend emerging methodolo-
Inference gies such as metamorphic testing, geometric probing, and
EnnCore sets the vision of delivering neural representa- abstract inference to systematize the internal properties and
tion models that are highly controlled regarding their in- consistency of controlled embedding spaces. Examples in-
ference properties. The key concept is to allow model de- clude the verification of abstract properties highly relevant to
velopers and domain experts to encode complex symbolic controlled inference such as monotonicity (Rozanova et al.
and geometric constraints within the models (safeguards), 2021) or variable substitution (Ferreira et al. 2021).
allowing for more controlled inference and better disentan- We also mention BayLIME (Zhao et al. 2020b), which is a
glement. Additionally, the project expands emerging prob- novel explainable AI tool enhancing the well-known LIME
ing and metamorphic testing methodologies to measure and tool with Bayesian reasoning to achieve better consistency
qualify the internal properties of the latent representation. in repeated explanations of a single prediction and better ro-
For this work-stream, we focus on designing controlled em- bustness to the hyper-parameters.
beddings for complex tasks in Natural Language Process-
ing (NLP), emphasizing textual entailment and question an- 5.3 Symbolic Verification Framework for AI
swering. These tasks allow for the design of models which Verification refers to algorithms that determine whether or
require the encoding of complex (i.e., requiring multiple se- not a model satisfies some pre-specified property. Symbolic
mantic operations) and multi-hop natural language inference verification algorithms compute the intermediate results us-
in an explainable manner. ing a symbolic representation – such as BDD, SAT, and
The inference control methods are represented as explicit SMT. Usually, symbolic verification scales better than ex-
linguistic and inference constraints, which elicit abductive plicit verification, thanks to its memory efficiency and ef-
inference biases that are integrated into the latent model. ficient computation. In the first year of EnnCore, we have
The intuition is that universal patterns of abstract inference, explored a few directions on the symbolic verification tech-
such as abstraction and fact unification (Valentino, Thaya- niques for AI, including working directly with the machine
paran, and Freitas 2021; Valentino, Pratt-Hartman, and Fre- learning models. The other two directions aim to deal with
itas 2021) can be programmed into the model, prescribing the scalability issues through abstract models and acceptable
an expected inference pattern, which can facilitate general- solutions safety, respectively.
ization but also enforce more consistent inferences. Follow- We considered two classes of machine learning mod-
ing the results achieved by encoding these constraints using els when working directly with the models. For convolu-
Integer Linear Programming (ILP) (Thayaparan, Valentino, tional neural networks (CNNs), a symbolic verification algo-
and Freitas 2020), which demonstrate its positive impact rithm based on interval analysis and symbolic layer-by-layer
on inference control and explainability, we proposed ∂- propagation was developed in (Yang et al. 2021; Li et al.
Explainer (Thayaparan et al. 2021), an end-to-end differen- 2020), together with a global optimisation based method
tiable architecture that integrates Convex Optimization such (Xu, Ruan, and Huang 2021). Second, for the random for-
as Linear Programming with neural representations for ab- est, an SMT-based method was considered to determine
ductive natural language inference. Specifically, we demon- whether a model has been data poisoned by a backdoor at-
strated that these models could integrate explicit inference tack (Huang, Zhao, and Huang 2020).
constraints with Transformers-based sentence representa- We also develop methods when scalability is an obstacle
tions and train the architecture end-to-end to improve expla- to the verification algorithms. For example, for deep rein-
nation generation and accuracy in multi-hop and abstractive forcement learning, we abstract its interactive behavior with
reasoning tasks. the environment into a discrete-time Markov chain and then
Part of the inference control mechanisms is expressed in apply an off-the-shelf probabilistic model checker to do ver-
ification (Dong, Zhao, and Huang 2021). For CNNs, we verification approaches that employ symbolic interval, e.g.,
abstracted a model into a Bayesian network and then con- Neurify (Wang et al. 2018).
ducted probabilistic inference as the verification algorithm As future work, we plan to work in two directions. First,
(Berthier et al. 2021a,b). we aim to evaluate security properties in various real case
We also deal with scalability from the perspective of ac- studies. Second, we will lead extensive experiments to val-
ceptable safety. In (Huang et al. 2021a), we developed a sta- idate the implementations of DNNs for a set of case stud-
tistical certification algorithm for the robustness of CNNs, ies from our industrial partners. This procedure requires us
and in (Zhao et al. 2021a,b), we considered an acceptable to set an environment for running the implementations of
level of reliability of CNNs. Moreover, coverage-guided DNNs in typical GPUs, which will rely on our prior work on
testing is proven an effective way to quantify the quality of the verification of GPU programs (Pereira et al. 2017). Ad-
a recurrent neural network (Huang et al. 2021b). ditionally, creating the benchmarks for the experiments is a
In addition to the above directions, we also developed our continuous and iterative task, consisting of two main steps:
views in (Ruan, Yi, and Huang 2021; Huang 2021), which (i) creating benchmarks using real applications of DNNs;
includes potential directions for exploration. and (ii) using industry-standard benchmarks in close collab-
oration with our partners. Lastly, we will interpret and vali-
5.4 Verifying Security in Embedded Software date the results obtained during these experiments and then
running in GPUs compare our approach using other state-of-the-art verifica-
We have developed and evaluated various verification strate- tion tools, similar to our recent work (Sena et al. 2021).
gies to detect errors in learning and classifications performed
by DNNs. In particular, we analyzed potential failures of 6 Conclusions
DNNs due to bugs in the implementation of the embedded
EnnCore contributes to the development of trustworthy
software of the DNNs. Here, we distinguish two classes of
neural-based systems, which are highly applicable to ar-
bugs: 1) generic implementation errors, for instance, mem-
eas of high societal impact, such as reliable infrastructure
ory safety, arithmetic overflow, and division-by-zero; they
management, defense, medical diagnosis and treatment, and
can cause the implementation of the DNN to crash; 2) failure
fair/unbiased decision making. In particular, EnnCore em-
of the implementation to behave according to the high-level
phasizes safety for medical diagnosis and treatment, with
rules, which may cause miss-classifications.
a use case targeting cancer. Personalized medicine requires
In (Sena et al. 2019, 2021), we develop and evaluate
the increasing use of automated data-driven methods. The
a novel symbolic verification framework using software
EnnCore project can directly impact the reduction of the
model checking (SMC) and satisfiability modulo theories
barriers to adopting AI-based methods in clinical settings,
(SMT) to check for safety properties in quantized neural
thereby democratizing personalized cancer diagnosis and
networks (QNNs). More specifically, we propose several
treatment. Additionally, one of our industrial partners is cur-
QNN-related optimizations for SMC, including invariant in-
rently acting as a blockchain-based supplier in the energy
ference via interval analysis, slicing, expression simplifica-
market. EnnCore tools will ensure the privacy and security
tions, and discretization of non-linear activation functions.
of the clients’ data in the energy sector. In particular, En-
We also quantified each technique’s impact using different
nCore will assist this industrial partner by providing inno-
SMT solvers. We observed a significant performance im-
vative methods to protect their customers’ data and applied
provement if we enabled slicing, interval analysis, and ex-
algorithms. As a result, we expect the EnnCore tools to push
pression simplifications with the SMT solver Yices (Sena
the state-of-the-art on formal verification and explainability
et al. 2021).
techniques to provide assurances about AI applications’ se-
With this verification framework, we also provide formal
curity and explain their security properties.
guarantees on the safe behavior of QNNs implemented both
in floating- and fixed-point arithmetic. In particular, we have
observed that the verification time correlates with the num- Acknowledgment
ber of bits used for ANN quantization. Interestingly, this The work is funded by EPSRC grant EP/T026995/1 enti-
correlation disappears for the number of bits above 14 due tled “EnnCore: End-to-End Conceptual Guarding of Neural
to the increasing state-space exploration. In this regard, our Architectures” under Security for all in an AI enabled soci-
verification approach was able to verify and produce ad- ety. Prof. Luján is funded by an Arm/RAEng Research Chair
versarial examples for 52 test cases spanning image clas- award and a Royal Society Wolfson Fellowship.
sification and general machine learning applications. Fur-
thermore, for small- to medium-sized QNNs, our approach References
completes most of its verification runs in minutes. In con-
trast to most state-of-the-art methods, our approach is not Albadi, M. H.; and El-Saadany, E. F. 2008. A summary of
restricted to specific choices regarding activation functions demand response in electricity markets. Electric power sys-
and non-quantized representations. Finally, our experiments tems research, 78(11): 1989–1996.
show that our approach can analyze larger ANN implemen- Alshahrani, M.; Khan, M. A.; Maddouri, O.; Kinjo, A. R.;
tations and substantially reduce the verification time com- Queralt-Rosinach, N.; and Hoehndorf, R. 2017. Neuro-
pared to state-of-the-art techniques that use SMT solving, symbolic representation learning on biological knowledge
e.g., Marabou (Kim et al. 2016). It is also competitive to graphs. Bioinformatics, 33(17): 2723–2730.
Berthier, N.; Alshareef, A.; Sharp, J.; Schewe, S.; and Gehr, T.; Mirman, M.; Drachsler-Cohen, D.; Tsankov, P.;
Huang, X. 2021a. Abstraction and Symbolic Execution Chaudhuri, S.; and Vechev, M. 2018. AI2: Safety and ro-
of Deep Neural Networks with Bayesian Approximation of bustness certification of neural networks with abstract inter-
Hidden Features. CoRR, abs/2103.03704. pretation. In IEEE S&P, 3–18.
Berthier, N.; Sun, Y.; Huang, W.; Zhang, Y.; Ruan, W.; and Hewitt, J.; and Liang, P. 2019. Designing and Interpreting
Huang, X. 2021b. Tutorials on Testing Neural Networks. Probes with Control Tasks. In EMNLP, 2733–2743.
CoRR, abs/2108.01734. Huang, C.; Fan, J.; Li, W.; Chen, X.; and Zhu, Q. 2019.
Bishop, C. M. 2006. Pattern recognition. Machine learning, ReachNN: Reachability Analysis of Neural-Network Con-
128(9). trolled Systems. ACM TECS, 18(5s).
Bonawitz, K.; Eichner, H.; Grieskamp, W.; Huba, D.; Inger- Huang, C.; Hu, Z.; Huang, X.; and Pei, K. 2021a. Statisti-
man, A.; Ivanov, V.; Kiddon, C.; Konečnỳ, J.; Mazzocchi, S.; cal Certification of Acceptable Robustness for Neural Net-
McMahan, H. B.; et al. 2019. Towards federated learning at works. In ICANN, 79–90.
scale: System design. CoRR, abs/1902.01046. Huang, W.; Sun, Y.; Zhao, X.; Sharp, J.; Ruan, W.; Meng, J.;
Briggs, C.; Fan, Z.; and Andras, P. 2020. Privacy Preserving and Huang, X. 2021b. Coverage-Guided Testing for Recur-
Demand Forecasting to Encourage Consumer Acceptance of rent Neural Networks. IEEE Tran. on Reliability, 1–16.
Smart Energy Meters. CoRR, abs/2012.07449. Huang, W.; Zhao, X.; and Huang, X. 2020. Embedding
and Extraction of Knowledge in Tree Ensemble Classifiers.
Capper, T.; Gorbatcheva, A.; Mustafa, M. A.; Bahloul, M.;
CoRR, abs/2010.08281.
Schwidtal, J. M.; et al. 2021. A Systematic Literature Re-
view of Peer-to-Peer, Community Self-Consumption, and Huang, X. 2021. Safety and reliability of deep learning:
Transactive Energy Market Models. Available at SSRN: (brief overview). In VARS, 1–2.
https://ssrn.com/abstract=3959620. Huang, X.; Kroening, D.; Ruan, W.; Sharp, J.; Sun, Y.;
Cordeiro, L.; Fischer, B.; and Marques-Silva, J. 2011. SMT- Thamo, E.; Wu, M.; and Yi, X. 2020. A survey of safety
based bounded model checking for embedded ANSI-C soft- and trustworthiness of deep neural networks: Verification,
ware. IEEE TSE, 38(4): 957–974. testing, adversarial attack and defence, and interpretability.
Computer Science Review, 37: 100270.
Cordeiro, L. C.; de Lima Filho, E. B.; and Bessa, I. V. 2020.
Survey on automated symbolic verification and its applica- Huang, X.; Kwiatkowska, M.; Wang, S.; and Wu, M. 2017.
tion for synthesising cyber-physical systems. IET Cyber- Safety verification of deep neural networks. In CAV, 3–29.
Physical Systems: Theory and Applications, 5(1): 1–24. Katz, G.; Barrett, C.; Dill, D. L.; Julian, K.; and Kochen-
derfer, M. J. 2017. Reluplex: An efficient SMT solver for
De Cristofaro, E. 2021. A critical overview of privacy in verifying deep neural networks. In CAV, 97–117.
machine learning. IEEE S&P, 19(4): 19–27.
Kim, Y.; Park, E.; Yoo, S.; Choi, T.; Yang, L.; and Shin, D.
Di, B.; Sun, J.; Chen, H.; and Li, D. 2020. Efficient Buffer 2016. Compression of Deep Convolutional Neural Networks
Overflow Detection on GPU. IEEE TPDS, 32(5): 1161– for Fast and Low Power Mobile Applications. In ICLR.
1177.
Lee, R.; Wysocki, O.; Zhou, C.; Calles, A.; Eastlake, L.;
Dong, Y.; Zhao, X.; and Huang, X. 2021. Dependability Ganatra, S.; Harrison, M.; et al. 2021. CORONET; COVID-
Analysis of Deep Reinforcement Learning based Robotics 19 in Oncology evaluatiON Tool: Use of machine learning
and Autonomous Systems. CoRR, abs/2109.06523. to inform management of COVID-19 in patients with cancer.
Doshi-Velez, F.; and Kim, B. 2017. Towards a rigor- Li, J.; Liu, J.; Yang, P.; Chen, L.; Huang, X.; and Zhang,
ous science of interpretable machine learning. CoRR, L. 2019. Analyzing Deep Neural Networks with Symbolic
abs/1702.08608. Propagation: Towards Higher Precision and Faster Verifica-
Dudjak, V.; Neves, D.; Alskaif, T.; Khadem, S.; Pena-Bello, tion. In Static Analysis, 296–319.
A.; Saggese, P.; Bowler, B.; Andoni, M.; Bertolini, M.; Li, R.; Li, J.; Huang, C.-C.; Yang, P.; Huang, X.; Zhang, L.;
Zhou, Y.; et al. 2021. Impact of local energy markets in- Xue, B.; and Hermanns, H. 2020. Prodeep: a platform for ro-
tegration in power systems layer: A comprehensive review. bustness verification of deep neural networks. In ESEC/FSE,
Applied Energy, 301: 117434. 1630–1634.
Eykholt, K.; Evtimov, I.; Fernandes, E.; Li, B.; Rahmati, A.; Lomuscio, A.; and Maganti, L. 2017. An approach to reach-
Xiao, C.; Prakash, A.; Kohno, T.; and Song, D. 2018. Robust ability analysis for feed-forward ReLU neural networks.
physical-world attacks on deep learning visual classification. CoRR, abs/1706.07351.
In CVPR, 1625–1634. Lundberg, S. M.; and Lee, S.-I. 2017. A unified approach to
Ferreira, D.; Rozanova, J.; Thayaparan, M.; Valentino, M.; interpreting model predictions. In NIPS, 4768–4777.
and Freitas, A. 2021. Does My Representation Capture X? Manhaeve, R.; Dumančić, S.; Kimmig, A.; Demeester, T.;
Probe-Ably. In ACL-IJCNLP, 194–201. and De Raedt, L. 2018. Deepproblog: Neural probabilistic
Garcez, A. d.; Gori, M.; Lamb, L. C.; Serafini, L.; Spranger, logic programming. CoRR, abs/1805.10872.
M.; and Tran, S. N. 2019. Neural-symbolic computing: An Melis, L.; Song, C.; De Cristofaro, E.; and Shmatikov, V.
effective methodology for principled integration of machine 2019. Exploiting unintended feature leakage in collaborative
learning and reasoning. CoRR, abs/1905.06088. learning. In IEEE S&P, 691–706.
Mercatali, G.; and Freitas, A. 2021. Disentangling Gener- Thayaparan, M.; Valentino, M.; Ferreira, D.; Rozanova, J.;
ative Factors in Natural Language with Discrete Variational and Freitas, A. 2021. ∂ -Explainer: Abductive Natural Lan-
Autoencoders. CoRR, abs/2109.07169. guage Inference via Differentiable Convex Optimization.
Miele, A. 2016. Buffer overflow vulnerabilities in CUDA: CoRR, abs/2105.03417.
a preliminary analysis. Journal of Computer Virology and Thayaparan, M.; Valentino, M.; and Freitas, A. 2020. Ex-
Hacking Techniques, 12(2): 113–120. planationLP: Abductive Reasoning for Explainable Science
Mirman, M.; Gehr, T.; and Vechev, M. 2018. Differentiable Question Answering. CoRR, abs/2010.13128.
abstract interpretation for provably robust neural networks. Valentino, M.; Pratt-Hartman, I.; and Freitas, A. 2021. Do
In ICML, 3578–3586. Natural Language Explanations Represent Valid Logical Ar-
Mustafa, M. A.; Cleemput, S.; and Abidin, A. 2016. A local guments? Verifying Entailment in Explainable NLI Gold
electricity trading market: Security analysis. In ISGT Eu- Standards. CoRR, abs/2105.01974.
rope, 1–6. Valentino, M.; Thayaparan, M.; and Freitas, A. 2021.
Nour, M.; Cömert, Z.; and Polat, K. 2020. A novel medical Unification-based Reconstruction of Multi-hop Explana-
diagnosis model for COVID-19 infection detection based on tions for Science Questions. In EACL, 200–211.
deep features and Bayesian optimization. Applied Soft Com- Wang, S.; Pei, K.; Whitehouse, J.; Yang, J.; and Jana, S.
puting, 97: 106580. 2018. Efficient Formal Safety Analysis of Neural Networks.
Odena, A.; Olsson, C.; Andersen, D.; and Goodfellow, In NeurIPS, 6369–6379.
I. 2019. Tensorfuzz: Debugging neural networks with Wicker, M.; Huang, X.; and Kwiatkowska, M. 2018.
coverage-guided fuzzing. In ICML, 4901–4911. Feature-guided black-box safety testing of deep neural net-
Pei, K.; Cao, Y.; Yang, J.; and Jana, S. 2017. DeepXplore: works. In TACAS, 408–426.
Automated whitebox testing of deep learning systems. In Wu, H.; Lv, D.; Cui, T.; Hou, G.; Watanabe, M.; and Kong,
SOSP, 1–18. ACM. W. 2021. SDLV: Verification of Steering Angle Safety for
Pereira, P.; Albuquerque, H.; da Silva, I.; Marques, H.; Self-Driving Cars. Formal Aspects of Computing, 33(3):
Monteiro, F.; Ferreira, R.; and Cordeiro, L. 2017. SMT- 325–341.
based context-bounded model checking for CUDA pro- Wu, M.; Wicker, M.; Ruan, W.; Huang, X.; and
grams. Concurrency and Computation: Practice and Ex- Kwiatkowska, M. 2020. A game-based approximate veri-
perience, 29(22): e3934. fication of deep neural networks with provable guarantees.
Rozanova, J.; Ferreira, D.; Thayaparan, M.; ; Valentino, M.; Theoretical Computer Science, 807: 298–329.
and Freitas, A. 2021. Supporting Context Monotonicity Ab- Xu, P.; Ruan, W.; and Huang, X. 2021. Towards the Quantifi-
stractions in Neural NLI Models. CoRR, abs/2105.08008. cation of Safety Risks in Deep Neural Networks. Complex
Ruan, W.; Huang, X.; and Kwiatkowska, M. 2018. Reach- and Intelligent Systems.
ability Analysis of Deep Neural Networks with Provable Yang, P.; Li, J.; Liu, J.; Huang, C.-C.; Li, R.; Chen, L.;
Guarantees. In IJCAI, 2651–2659. Huang, X.; and Zhang, L. 2021. Enhancing robustness veri-
Ruan, W.; Wu, M.; Sun, Y.; Huang, X.; Kroening, D.; and fication for deep neural networks via symbolic propagation.
Kwiatkowska, M. 2019. Global Robustness Evaluation of Formal Aspects of Computing, 1–29.
Deep Neural Networks with Provable Guarantees for the Zhao, X.; Banks, A.; Sharp, J.; Robu, V.; Flynn, D.; Fisher,
Hamming Distance. In IJCAI, 5944–5952. M.; and Huang, X. 2020a. A Safety Framework for Crit-
Ruan, W.; Yi, X.; and Huang, X. 2021. Adversarial Robust- ical Systems Utilising Deep Neural Networks. In Safe-
ness of Deep Learning: Theory, Algorithms, and Applica- Comp2020, 244–259.
tions. In ACM CIKM, 4866–4869. Zhao, X.; Huang, W.; Banks, A.; Cox, V.; Flynn, D.;
Sattler, F.; Müller, K.-R.; and Samek, W. 2021. Clustered Schewe, S.; and Huang, X. 2021a. Assessing the Reliability
Federated Learning: Model-Agnostic Distributed Multitask of Deep Learning Classifiers Through Robustness Evalua-
Optimization Under Privacy Constraints. IEEE TNNLS, tion and Operational Profiles. CoRR, abs/2106.01258.
32(8): 3710–3722. Zhao, X.; Huang, W.; Huang, X.; Robu, V.; and Flynn,
Sena, L.; Song, X.; Alves, E.; Bessa, I.; Manino, E.; and D. 2020b. Baylime: Bayesian local interpretable model-
Cordeiro, L. 2021. Verifying Quantized Neural Networks agnostic explanations. CoRR, abs/2012.03058.
using SMT-Based Model Checking. CoRR, abs/2106.05997. Zhao, X.; Huang, W.; Schewe, S.; Dong, Y.; and Huang, X.
Sena, L. H.; Bessa, I. V.; Gadelha, M. R.; Cordeiro, L. C.; 2021b. Detecting Operational Adversarial Examples for Re-
and Mota, E. 2019. Incremental Bounded Model Checking liable Deep Learning. CoRR, abs/2104.06015.
of Artificial Neural Networks in CUDA. In SBESC, 1–8. Zheng, S.; Song, Y.; Leung, T.; and Goodfellow, I. 2016. Im-
Sun, Y.; Huang, X.; Kroening, D.; Sharp, J.; Hill, M.; and proving the robustness of deep neural networks via stability
Ashmore, R. 2019. Structural Test Coverage Criteria for training. In CVPR, 4480–4488.
Deep Neural Networks. ACM TECS, 18(5s): 1–23.
Sun, Y.; Wu, M.; Ruan, W.; Huang, X.; Kwiatkowska, M.;
and Kroening, D. 2018. Concolic testing for deep neural
networks. In ASE, 109–119.