Many works have demonstrated that neural networks are vulnerable to adversarial examples. We examine the adversarial sticker attack, where the attacker places a sticker somewhere on an image to induce it to be misclassified. We take a first step towards defending against such attacks using clipped BagNet, which bounds the influence that any limited-size sticker can have on the final classification. We evaluate our scheme on ImageNet and show that it provides strong security against targeted PGD attacks and gradient-free attacks, and yields certified security for a 95% of images against a targeted 20 × 20 pixel attack.

Deep learning image classification is vulnerable to adversarial attack, even if the attacker changes just a small patch of the image. We propose a defense against patch attacks based on partially occluding the image around each candidate patch location, so that a few occlusions each completely hide the patch. We demonstrate on CIFAR-10, Fashion MNIST, and MNIST that our defense provides certified security against patch attacks of a certain size.

Adversarial examples allow crafted attacks against deep neural network classification of images. We propose a defense of expanding the training set with a single, large, and diverse class of background images, striving to `fill' around the borders of the classification boundary. We find it aids detection of simple attacks on EMNIST, but not advanced attacks. We discuss several limitations of our examination.

Machine learning is increasingly used to make sense of the physical world yet may suffer from adversarial manipulation. We examine the Viola-Jones 2D face detection algorithm to study whether images can be created that humans do not notice as faces yet the algorithm detects as faces. We show that it is possible to construct images that Viola-Jones recognizes as containing faces yet no human would consider a face. Moreover, we show that it is possible to construct images that fool facial detection even when they are printed and then photographed.

Hypervisors provide a security foundation of cloud computing, yet have suffered exploits. Efforts at formal verification have included codevelopment (XMHF) and interactive theorem proving (seL4). A technique that can be quickly applied to existing hypervisors is desirable. We examine binaries by extending the Binary Analysis Platform (BAP) to include the required system mode instructions used by hypervisors. We translate the BAP output to Boogie, a language which is then converted to an SMT formula, and define a security property that the hypervisor response to guest execution does not modify the hypervisor code pages. We use BAP and Boogie to automatically detect one ported and two injected bugs and verify that 1000 random traces through the intercept handler do not violate our property. We identify constructs that are difficult to verify automatically. Our tool should be usable in analyzing other hypervisors.

Virtualization promises significant benefits in security, efficiency, dependability, and cost. Achieving these benefits depends upon the reliability of the underlying hyper visor. Hyper visors provide complete control of the virtualized resources (protection), a reasonably accurate view of these resources (fidelity), and performance. To facilitate formal verification of protection, we present an architecture, aligned with the hardware virtualization barrier, that separates hyper visor protection from the other goals. The hyper visor is constructed on a minimal trusted computing base or "min visor" whose main responsibility is protection. Each real guest is paired with an untrusted fidelity guest that builds on the protection layer to provide a fully virtualized environment. This allows verification of protection without considering much of the functionality of a traditional hyper visor. We have coded such a protection layer, developed a simple hyper visor on it, and begun formally verifying its protection properties at the machine code level. The current paper is a progress report.

Modeling is the crucial first step in formal verification. Some models are constructed by humans from source code, while others are extracted automatically by tools. Regardless of how a model is constructed, verification is only as good as the model; therefore, it is essential to validate the model against the implementation it represents. In this paper we present two complementary approaches to software model validation. The first, data-centric model validation, checks that, for data structures relevant to the property being verified, all operations that update these data structures are captured in the model. The second, operation-centric model validation, checks that each operation being modeled is correctly simulated by the model. Both techniques are based on a combination of symbolic execution and satisfiability modulo theories (SMT) solving. We demonstrate the application of our methods on several case studies, including the address translation logic in the Bochs x86 emulator, the Berkeley Packet Filter, a TCAS benchmark suite, the FTP server from GNU Inetutils, and a component of the XMHF hypervisor.

Virtualization promises significant benefits in security, efficiency, dependability, and cost. Achieving these benefits depends upon the reliability of the underlying virtual machine monitors (hypervisors). This paper describes an ongoing project to develop and verify MinVisor, a simple but functional Type-I x86 hypervisor, proving protection properties at the assembly level using ACL2. Originally based on an existing research hypervisor, MinVisor provides protection of its own memory from a malicious guest. Our long-term goal is to fully verify MinVisor, providing a vehicle to investigate the modeling and verification of hypervisors at the implementation level, and also a basis for further systems research. Functional segments of the MinVisor C code base are translated into Y86 assembly, and verified with respect to the Y86 model. The inductive assertions (also known as compositional cutpoints) methodology is used to prove the correctness of the code. The proof of the code that sets up the nested page tables is described. We compare this project to related efforts in systems code verification and outline some useful steps forward.