TL;DR
This paper presents tools and frameworks for automatically generating, validating, and monitoring IoT device network behavior profiles (MUD profiles) to enhance security and policy compliance.
Contribution
It introduces an open-source tool for automatic MUD profile generation from traffic traces and a formal framework for validating and verifying MUD profiles against organizational policies.
Findings
Successfully generated MUD profiles for 28 IoT devices
Validated MUD profiles for consistency and policy compatibility
Demonstrated dynamic device identification and behavior monitoring
Abstract
IoT devices are increasingly being implicated in cyber-attacks, raising community concern about the risks they pose to critical infrastructure, corporations, and citizens. In order to reduce this risk, the IETF is pushing IoT vendors to develop formal specifications of the intended purpose of their IoT devices, in the form of a Manufacturer Usage Description (MUD), so that their network behavior in any operating environment can be locked down and verified rigorously. This paper aims to assist IoT manufacturers in developing and verifying MUD profiles, while also helping adopters of these devices to ensure they are compatible with their organizational policies and track devices network behavior based on their MUD profile. Our first contribution is to develop a tool that takes the traffic trace of an arbitrary IoT device as input and automatically generates the MUD profile for it. We…
Click any figure to enlarge with its caption.
Figure 1
Figure 2
Figure 3
Figure 4
Figure 5
Figure 6
Figure 7
Figure 8
Figure 9
Figure 10
Figure 11
Figure 12
Figure 13
Figure 14
Figure 15
Figure 16
Figure 17
Figure 18
Figure 19
Figure 20
Figure 21
Figure 22
Figure 23
Figure 24Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Verifying and Monitoring IoTs Network Behavior using MUD Profiles
Ayyoob Hamza, Dinesha Ranathunga, Hassan Habibi Gharakheili,
Theophilus A. Benson, Matthew Roughan, and Vijay Sivaraman
A. Hamza, H. Habibi Gharakheili, and V. Sivaraman are with the School of Electrical Engineering and Telecommunications, University of New South Wales, Sydney, NSW 2052, Australia (e-mails: [email protected], [email protected], [email protected]). D. Ranathunga and M. Roughan are with the the School of Mathematical Sciences, University of Adelaide, SA, 5005, Australia (e-mails: [email protected], [email protected]). T. Benson is with the School of Computer Science and Engineering, Brown University, Providence, RI 02192, USA (e-mail: [email protected]). This submission is an extended and improved version of our paper presented at the ACM Workshop on IoT S&P 2018 [IoTSnP18].
Abstract
IoT devices are increasingly being implicated in cyber-attacks, raising community concern about the risks they pose to critical infrastructure, corporations, and citizens. In order to reduce this risk, the IETF is pushing IoT vendors to develop formal specifications of the intended purpose of their IoT devices, in the form of a Manufacturer Usage Description (MUD), so that their network behavior in any operating environment can be locked down and verified rigorously.
This paper aims to assist IoT manufacturers in developing and verifying MUD profiles, while also helping adopters of these devices to ensure they are compatible with their organizational policies and track devices network behavior based on their MUD profile. Our first contribution is to develop a tool that takes the traffic trace of an arbitrary IoT device as input and automatically generates the MUD profile for it. We contribute our tool as open source, apply it to 28 consumer IoT devices, and highlight insights and challenges encountered in the process. Our second contribution is to apply a formal semantic framework that not only validates a given MUD profile for consistency, but also checks its compatibility with a given organizational policy. We apply our framework to representative organizations and selected devices, to demonstrate how MUD can reduce the effort needed for IoT acceptance testing. Finally, we show how operators can dynamically identify IoT devices using known MUD profiles and monitor their behavioral changes on their network.
Index Terms:
IoT, MUD, Policy Verification, Device Discovery, Compromised Device Detection
I Introduction
The Internet of Things is considered the next technological mega-trend, with wide reaching effects across the business spectrum [sachs2014]. By connecting billions of every day devices Ð from smart watches to industrial equipment Ð to the Internet, IoT integrates the physical and cyber worlds, creating a host of opportunities and challenges for businesses and consumers alike. But, increased interconnectivity also increases the risk of using these devices.
Many connected IoT devices can be found on search engines such as Shodan [Shodan], and their vulnerabilities exploited at scale. For example, Dyn, a major DNS provider, was subjected to a DDoS attack originating from a large IoT botnet comprising thousands of compromised IP-cameras [Dyn16]. IoT devices, exposing TCP/UDP ports to arbitrary local endpoints within a home or enterprise, and to remote entities on the wider Internet, can be used by inside and outside attackers to reflect/amplify attacks and to infiltrate otherwise secure networks[Wisec17]. IoT device security is thus a top concern for the Internet ecosystem.
These security concerns have prompted standards bodies to provide guidelines for the Internet community to build secure IoT devices and services [DHS16, NIST16, ENISA17], and for regulatory bodies (such as the US FCC) to control their use [FCC16]. The focus of our work is an IETF proposal called Manufacturer Usage Description (MUD) [ietfMUD18] which provides the first formal framework for IoT behavior that can be rigorously enforced. This framework requires manufacturers of IoTs to publish a behavioral profile of their device, as they are the ones with best knowledge of how their device will behave when installed in a network; for example, an IP camera may need to use DNS and DHCP on the local network, and communicate with NTP servers and a specific cloud-based controller in the Internet, but nothing else. Such requirements vary across IoTs from different manufacturers. Knowing each device’s requirements will allow network operators to impose a tight set of access control list (ACL) restrictions for each IoT device in operation, so as to reduce the potential attack surface on their network.
The MUD proposal hence provides a light-weight model to enforce effective baseline security for IoT devices by allowing a network to auto-configure the required network access for the devices, so that they can perform their intended functions without having unrestricted network privileges.
MUD is a new and emerging paradigm, and there is little collective wisdom today on how manufacturers should develop behavioral profiles of their IoT devices, or how organizations should use these profiles to secure their network and monitor the runtime behaviour of IoT devices. Our preliminary work in [hamza2018] was one of the first attempts to address these shortcomings. This paper111This project was supported by Google Faculty Research Awards Centre of Excellence for Mathematical and Statistical Frontiers (ACEMS). significantly expands on our prior work by proposing an IoT device classification framework which uses observed traffic traces and incrementally compares them with known IoT MUD signatures. We use this framework and trace data captured over a period of six months from a test-bed comprising of 28 distinct IoT devices to identify (a) legacy IoT devices without vendor MUD support; (b) IoT devices with outdated firmware; and (c) IoT devices which are potentially compromised. To the best of our knowledge, this is the first attempt to automatically generate MUD profiles, formally check their consistency and compatibility with an organizational policy, prior to deployment. In summary, our contributions are:
- •
We instrument a tool to assist IoT manufacturers to generate MUD profiles. Our tool takes as input the packet trace containing the operational behavior of an IoT device, and generates as ouput a MUD profile for it. We contribute our tool as open source[mudgenerator], apply it to 28 consumer IoT devices, and highlight insights and challenges encountered in the process.
- •
We apply a formal semantic framework that not only validates a given MUD profile for consistency, but also checks its compatibility with a given organizational policy. We apply our semantic framework to representative organizations and selected devices, and demonstrate how MUD can greatly simplify the process of IoT acceptance into the organization.
- •
We propose an IoT device classification framework using observed traffic traces and known MUD signatures to dynamically identify IoT devices and monitor their behavioral changes in a network.
The rest of the paper is organized as follows: §II describes relevant background work on IoT security and formal policy modeling. §III describes our open-source tool for automatic MUD profile generation. Our verification framework for MUD policies is described in §IV, followed by evaluation of results. We describe our IoT device classification framework in §LABEL:sec:dynProf and demonstrate its use to identify and monitor IoT behavioral changes within a network. We conclude the paper in §LABEL:sec:con.
II Background and Related Work
Securing IoT devices has played a secondary role to innovation, i.e., creating new IoT functionality (devices and services). This neglection of security has created a substantial safety and economic risks for the Internet [Survey17]. Today many manufacturer IoT devices lack even the basic security measures [IoTSnp17] and network operators have poor visibility into the network activity of their connected devices hindering the application of access-control policies to them [CiscoReport18]. IoT botnets continue to grow in size and sophistication and attackers are leveraging them to launch large-scale DDoS attacks [f5Labs17]; devices such as baby monitors, refrigerators and smart plugs have been hacked and controlled remotely [sivaraman2016smart]; and many organizational assets such as cameras are being accessed publicly [SonyCam, Insecam18].
Existing IoT security guidelines and recommendations [DHS16, NIST16, ENISA17, FCC16] are largely qualitative and subject to human interpretation, and therefore unsuitable for automated and rigorous application. The IETF MUD specification [ietfMUD18] on the other hand defines a formal framework to capture device run-time behavior, and is therefore amenable to rigorous evaluation. IoT devices also often have a small and recognizable pattern of communication (as demonstrated in our previous work [SmartCity17]). Hence, the MUD proposal allows IoT device behaviour to be captured succinctly, verified formally for compliance with organizational policy, and assessed at run-time for anomalous behavior that could indicate an ongoing cyber-attack.
A valid MUD profile contains a root object called “access-lists” container [ietfMUD18] which comprise of several access control entries (ACEs), serialized in JSON format. Access-lists are explicit in describing the direction of communication, i.e., from-device and to-device. Each ACE matches traffic on source/destination port numbers for TCP/UDP, and type and code for ICMP. The MUD specifications also distinguish local-networks traffic from Internet communications.
We provide here a brief background on the formal modeling and verification framework used in this paper. We begin by noting that the lack of formal policy modeling in current network systems contribute to frequent misconfigurations [wool2010, ranathunga2016T, ranathunga2016G]. We use the concept of a metagraph, which is a generalized graph-theoretic structure that offers rigorous formal foundations for modeling and analyzing communication-network policies in general. A metagraph is a directed graph between a collection of sets of “atomic” elements [basu2007]. Each set is a node in the graph and each directed edge represents the relationship between two sets. Fig. 1 shows an example where a set of users () are related to sets of network resources (, , ) by the edges and describing which user is allowed to access resource .
Metagraphs can also have attributes associated with their edges. An example is a conditional metagraph which includes propositions – statements that may be true or false – assigned to their edges as qualitative attributes [basu2007]. The generating sets of these metagraphs are partitioned into a variable set and a proposition set. A conditional metagraph is formally defined as follows:
Definition 1** (Conditional Metagraph).**
*A conditional metagraph is a metagraph = in which is a set of propositions and is a set of variables, and:
-
at least one vertex is not null, i.e.,
-
the invertex and outvertex of each edge must be disjoint, i.e., with
-
an outvertex containing propositions cannot contain other elements, i.e., , if , then .*
Conditional metagraphs enable the specification of stateful network-policies and have several useful operators. These operators readily allow one to analyze MUD policy properties like consistency.
The MUD proposal defines how a MUD profile needs to be fetched. The MUD profile will be downloaded using a MUD url (*e.g., *via DHCP option). For legacy devices already in production networks, MUD specifications suggest to create a mapping of those devices to their MUD url. Therefore, in this paper, we develop a method (in §LABEL:sec:dynProf) for automatic device identification using MUD profiles to reduce the complexity of manual mapping a device to its corresponding MUD-url.
Past works have employed machine learning to classify IoT devices for asset management [meidan2017, sivanathan2018]. Method in [meidan2017] employs over 300 attributes (packet-level and flow-level), though the most influential ones are minimum, median, and average of packet volume, Time-To-Live (TTL), the ratio of total bytes transmitted and received, and the total number of packets with RST flag reset. Work in [sivanathan2018] proposes to use features with less computation cost at runtime. Existing Machine learning based proposals need to re-train their model when a new device type is added – this limits the usability in terms of not being able to transfer the models across deployments.
While all the above works make important contributions, they do not leverage the MUD proposal, which the IETF is pushing for vendors to adopt. We overcome the shortfall by developing an IoT device classification framework which dynamically compares the device traffic traces (run-time network behavior) with known static IoT MUD signatures. Using this framework, we are able to identify (a) legacy IoT devices without vendor MUD support; (b) IoT devices with outdated firmware; and (c) IoT devices which are potentially compromised.
III MUD Profile Generation
The IETF MUD specification is still evolving as a draft. Hence, IoT device manufacturers have not yet provided MUD profiles for their devices. We, therefore, developed a tool – MUDgee – which automatically generates a MUD profile for an IoT device from its traffic trace in order to make this process faster, cheaper and more accurate. In this section, we describe the structure of our open source tool [mudgenerator], apply it to traces of 28 consumer IoT devices, and highlight insights.
We captured traffic flows for each IoT device during a six month observation period, to generate our MUD rules. The IETF MUD draft allows both ‘allow’ and ‘drop’ rules. In our work, instead, we generate profiles that follow a whitelisting model (*i.e., *only ‘allow’ rules with default ‘drop’). Having a combination of ‘accept’ and ‘drop’ rules requires a notion of rule priority (*i.e., *order) and is not supported by the current IETF MUD draft. For example, Table I shows traffic flows observed for a Blipcare blood pressure monitor. The device only generates traffic whenever it is used. It first resolves its intended server at tech.carematrix.com by exchanging a DNS query/response with the default gateway (*i.e., *the top two flows). It then uploads the measurement to its server operating on TCP port 8777 (described by the bottom two rules).
III-A MUDgee Architecture
MUDgee implements a programmable virtual switch (vSwitch) with a header inspection engine attached and plays an input PCAP trace (of an arbitrary IoT device) into the switch. MUDgee has two separate modules; (a) captures and tracks all TCP/UDP flows to/from device, and (b) composes a MUD profile from the flow rules. We describe these two modules in detail below.
Capture intended flows: Consumer IoT devices use services provided by remote cloud servers and also expose services to local hosts (*e.g., *a mobile App). We track (intended) both remote and local device communications using separate flow rules to meet the MUD specification requirements.
It is challenging to capture services (*i.e., *especially those operating on non-standard TCP/UDP ports) that a device is either accessing or exposing. This is because local/remote services operate on static port numbers whereas source port numbers are dynamic (and chosen randomly) for different flows of the same service. We note that it is trivial to deduce the service for TCP flows by inspecting the SYN flag, but not so easy for UDP flows. We, therefore, developed an algorithm (Fig. 2) to capture bidirectional flows for an IoT device.
We first configure the vSwitch with a set of proactive rules, each with a specific action (*i.e., *“forward” or “mirror”) and a priority (detailed rules can be found in our technical report [hamza2018]). Proactive rules with a ‘mirror’ action will feed the header inspection engine with a copy of the matched packets. Our inspection algorithm, shown in Fig. 2, will insert a corresponding reactive rule into the vSwitch.
Our algorithm matches a DNS reply to a top priority flow and extracts and stores the domain name and its associated IP address in a DNS cache. This cache is dynamically updated upon arrival of a DNS reply matching an existing request.
The MUD specification also requires the segregation of traffic to and from a device for both local and Internet communications. Hence, our algorithm assigns a unique priority to the reactive rules associated with each of the groups: from-local, to-local, from-Internet and to-Internet. We use a specific priority for flows that contain a TCP SYN to identify if the device or the remote entity initiated the communication.
Flow translation to MUD: MUDgee uses the captured traffic flows to generate a MUD profile for each device. We convert each flow to a MUD ACE by considering the following:
Consideration 1: We reverse lookup the IP address of the remote endpoint and identify the associated domain name (if any), using the DNS cache.
Consideration 2: Some consumer IoTs, especially IP cameras, typically use the STUN (STUN) protocol to verify that the user’s mobile app can stream video directly from the camera over the Internet. If a device uses the STUN protocol over UDP, we must allow all UDP traffic to/from Internet servers because the STUN servers often require the client device to connect to different IP addresses or port numbers.
Consideration 3: We observed that several smart IP cameras communicate with many remote servers operating on the same port (*e.g., *Belkin Wemo switch). However, no DNS responses were found corresponding to the server IP addresses. So, the device must obtain the IP address of its servers via a non-standard channel (*e.g., *the current server may instruct the device with the IP address of the subsequent server). If a device communicates with several remote IP addresses (*i.e., *more than our threshold value of five), all operating on the same port, we allow remote traffic to/from any IP addresses (*i.e., **) on that specific port number.
Consideration 4: Some devices (*e.g., *TPLink plug) use the default gateway as the DNS resolver, and others (*e.g., *Belkin WeMo motion) continuously ping the default gateway. The existing MUD draft maps local communication to fixed IP addresses through the controller construct. We consider the local gateway to act as the controller, and use the name-space urn:ietf:params:mud:gateway for the gateway.
The generated MUD profiles of the 28 consumer IoT devices in our test bed are listed in Table II and are publicly available at: https://iotanalytics.unsw.edu.au/mud/.
III-B Insights and challenges
The Blipcare BP monitor is an example device with static functionalities. It exchanges DNS queries/responses with the local gateway and communicates with a single domain name over TCP port 8777. So its behavior can be locked down to a limited set of static flow rules. The majority of IoT devices that we tested (*i.e., *22 out of 28) fall into this category (marked in green in Table II).
We use Sankey diagrams (shown in Fig. 3) to represent the MUD profiles in a human-friendly way. The second category of our generated MUD profiles is exemplified by Fig. 3(a). This Sankey diagram shows how the TP-Link camera accesses/exposes limited ports on the local network. The camera gets its DNS queries resolved, discovers local network using mDNS over UDP 5353, probes members of certain multicast groups using IGMP, and exposes two TCP ports 80 (management console) and 8080 (unicast video streaming) to local devices. All these activities can be defined by a tight set of ACLs.
But, over the Internet, the camera communicates to its STUN server, accessing an arbitrary range of IP addresses and port numbers shown by the top flow. Due to this communication, the functionality of this device can only be loosely defined. Devices that fall in to this category (*i.e., *due to the use of STUN protocol), are marked in blue in Table II. The functionality of these devices can be more tightly defined if manufacturers of these devices configure their STUN servers to operate on a specific set of endpoints and port numbers, instead of a broad and arbitrary range.
Amazon Echo, represents devices with complex and dynamic functionality, augmentable using custom recipes or skills. Such devices (marked in red in Table II), can communicate with a growing range of endpoints on the Internet, which the original manufacturer cannot define in advance. For example, our Amazon Echo interacts with the Hue lightbulb
in our test bed by communicating with meethue.com over TCP 443. It also contacts the news website abc.net.au when prompted by the user. For these type of devices, the biggest challenge is how manufacturers can dynamically update their MUD profiles to match the device capabilities. But, even the initial MUD profile itself can help setup a minimum network-communication permissions set that can be amended over time.
IV MUD profile verification
Network operators should not allow a device to be installed in their network, without first checking its compatibility with the organisation’s security policy. We’ve developed a tool – MUDdy – which can help with the task. MUDdy can check an IoT device’s MUD profile is correct syntactically and semantically and ensure that only devices which are compliant and have MUD signatures that adhere to the IETF proposal are deployed in a network.
IV-A Syntactic correctness
A MUD profile comprises of a YANG model that describes device-specific network behavior. In the current version of MUD, this model is serialized using JSON [ietfMUD18] and this serialisation is limited to a few YANG modules (*e.g., *ietf-access-control-list). MUDdy raises an invalid syntax exception when parsing a MUD profile if it detects any schema beyond these permitted YANG modules.
MUDdy also rejects MUD profiles containing IP addresses with local significance. The IETF advises MUD-profile publishers to utilise the high-level abstractions provided in the MUD proposal and avoid using hardcoded private IP addresses [ietfMUD18]. MUDdy also discards MUD profiles containing access-control actions other than ‘accept’ or ‘drop’.
IV-B Semantic correctness
Checking a MUD policy’s syntax partly verifies its correctness. A policy must additionally be semantically correct; so we must check a policy, for instance, for inconsistencies.
Policy inconsistencies can produce unintended consequences [wool2004] and in a MUD policy, inconsistencies can stem from (a) overlapping rules with different access-control actions; and/or (b) overlapping rules with identical actions. The MUD proposal excludes rule ordering, so, the former describes ambiguous policy-author intent (*i.e., *intent-ambiguous rules). In comparison, the latter associates a clear (single) outcome and describes redundancies. Our adoption of an application-whitelisting model prevents the former by design, but, redundancies are still possible and need to be checked.
MUDdy models a MUD policy using a metagraph underneath. This representation enables us to use Metagraph algebras [basu2007] to precisely check the policy model’s consistency. It’s worth noting here that past works [al2005] classify policy consistency based on the level of policy-rule overlap. But, these classifications are only meaningful when the policy-rule order is important (*e.g., *in a vendor-device implementation). However, rule order is not considered in the IETF MUD proposal and it is also generally inapplicable in the context of a policy metagraph. Below is a summary description of the process we use to check the consistency of a policy model.
IV-B1 Policy modeling
Access-control policies are often represented using the five-tuple: source/destination address, protocol, source/destination ports [cisco2013, juniper2016, palo2017]. We construct MUD policy metagraph models leveraging this idea. Fig. 4 shows an example for a Lifx bulb. Here, the source/destination addresses are represented by the labels device, local-network, local-gateway and a domain-name (*e.g., *pool.ntp.org). Protocol and ports are propositions of the metagraph.
IV-B2 Policy definition and verification
We wrote MGtoolkit [ranathunga2017] – a package for implementing metagraphs – to instantiate our policy models. MGtoolkit is implemented in Python 2.7. The API allows users to create metagraphs, apply metagraph operations and evaluate results.
Mgtoolkit provides a ConditionalMetagraph class which extends a Metagraph and supports propositions. The class inherits the members of a Metagraph and additionally supports methods to check consistency. We use this class to instantiate our MUD policy models and check their consistency.
Our verification of metagraph consistency uses dominance [basu2007] which can be introduced constructively as follows:
Definition 2** (Edge-dominant Metapath).**
Given a metagraph = for any two sets of elements and in , a metapath is said to be edge-dominant if no proper subset of is also a metapath from to .
Definition 3** (Input-dominant Metapath).**
Given a metagraph = for any two sets of elements and in , a metapath is said to be input-dominant if there is no metapath such that .
In other words, edge-dominance (input-dominance) ensures that none of the edges (elements) in the metapath are redundant. These concepts allow us to define a dominant metapath as per below. A non-dominant metapath indicates redundancy in the policy represented by the metagraph.
Definition 4** (Dominant Metapath).**
Given a metagraph = for any two sets of elements and in , a metapath is said to be dominant if it is both edge dominant and input-dominant.
IV-B3 Compatibility with best practices
MUD policy consistency checks partly verify if it is semantically correct. In addition, a MUD policy may need to be verified against a local security policy or industry recommended practices (such as the ANSI/ISA- 62443-1-1), for compliance. Doing so, is critical when installing an IoT device in a mission-critical network such as a SCADA network, where highly restrictive cyber-security practices are required to safeguard people from serious injury or even death!
We built an example organisational security policy based on SCADA best practice guidelines to check MUD policy compliance. We chose these best practices because they offer a wide spectrum of policies representative of various organisations. For instance, they include policies for the highly protected SCADA zone (which, for instance, might run a power plant) as well as the more moderately-restrictive Enterprise zone.
We define a MUD policy rule to be SCADA (or Enterprise) zone compatible if its corresponding traffic flow complies with SCADA (or Enterprise) best practice policy. For instance, a MUD rule which permits a device to communicate with the local network using DNS complies with the Enterprise zone policy. But, a rule enabling device communication with an Internet server using HTTP violates the SCADA zone policy.
Our past work has investigated the problem of policy comparison using formal semantics, in the SCADA domain for firewall access-control policies [ranathunga2016P]. We adapt the methods and algebras developed there, to also check MUD policies against SCADA best practices. Key steps enabling these formal comparisons are summarized below.
Policies are mapped into a unique canonical decomposition. Policy canonicalisation can be represented through a mapping , where is the policy space and is the canonical space of policies. All equivalent policies of map to a singleton. For , we note the following (the proof follows the definition)
Lemma 5**.**
Policies iff .
MUD policy compliance can be checked by comparing canonical policy components. For instance
Is ?
A notation also useful in policy comparison is that policy includes policy . In SCADA networks, the notation helps evaluate whether a MUD policy is compliant with industry-recommended practices in [stouffer2008, byres2005]. A violation increases the vulnerability of a SCADA zone to cyber attacks.
We indicate that a policy complies with another if it is more restrictive or included in and define the following
Definition 6** (Inclusion).**
A policy is included in on iff , i.e., either has the same effect as on , or denies , for all . We denote inclusion by .
A MUD policy () can be checked against a SCADA best practice policy () for compliance using inclusion
Is ?
The approach can also be used to check if a MUD policy complies with an organisation’s local security policy, to ensure that IoT devices are plug and play enabled, only in the compatible zones of the network.
IV-C Verification results
