-
Verifying RISC-V Physical Memory Protection
Authors:
Kevin Cheang,
Cameron Rasmussen,
Dayeol Lee,
David W. Kohlbrenner,
Krste Asanović,
Sanjit A. Seshia
Abstract:
We formally verify an open-source hardware implementation of physical memory protection (PMP) in RISC-V, which is a standard feature used for memory isolation in security critical systems such as the Keystone trusted execution environment. PMP provides per-hardware-thread machine-mode control registers that specify the access privileges for physical memory regions. We first formalize the functiona…
▽ More
We formally verify an open-source hardware implementation of physical memory protection (PMP) in RISC-V, which is a standard feature used for memory isolation in security critical systems such as the Keystone trusted execution environment. PMP provides per-hardware-thread machine-mode control registers that specify the access privileges for physical memory regions. We first formalize the functional property of the PMP rules based on the RISC-V ISA manual. Then, we use the LIME tool to translate an open-source implementation of the PMP hardware module written in Chisel to the UCLID5 formal verification language. We encode the formal specification in UCLID5 and verify the functional correctness of the hardware. This is an initial effort towards verifying the Keystone framework, where the trusted computing base (TCB) relies on PMP to provide security guarantees such as integrity and confidentiality.
△ Less
Submitted 3 November, 2022;
originally announced November 2022.
-
Cerberus: A Formal Approach to Secure and Efficient Enclave Memory Sharing
Authors:
Dayeol Lee,
Kevin Cheang,
Alexander Thomas,
Catherine Lu,
Pranav Gaddamadugu,
Anjo Vahldiek-Oberwagner,
Mona Vij,
Dawn Song,
Sanjit A. Seshia,
Krste Asanović
Abstract:
Hardware enclaves rely on a disjoint memory model, which maps each physical address to an enclave to achieve strong memory isolation. However, this severely limits the performance and programmability of enclave programs. While some prior work proposes enclave memory sharing, it does not provide a formal model or verification of their designs. This paper presents Cerberus, a formal approach to secu…
▽ More
Hardware enclaves rely on a disjoint memory model, which maps each physical address to an enclave to achieve strong memory isolation. However, this severely limits the performance and programmability of enclave programs. While some prior work proposes enclave memory sharing, it does not provide a formal model or verification of their designs. This paper presents Cerberus, a formal approach to secure and efficient enclave memory sharing. To reduce the burden of formal verification, we compare different sharing models and choose a simple yet powerful sharing model. Based on the sharing model, Cerberus extends an enclave platform such that enclave memory can be made immutable and shareable across multiple enclaves via additional operations. We use incremental verification starting with an existing formal model called the Trusted Abstract Platform (TAP). Using our extended TAP model, we formally verify that Cerberus does not break or weaken the security guarantees of the enclaves despite allowing memory sharing. More specifically, we prove the Secure Remote Execution (SRE) property on our formal model. Finally, the paper shows the feasibility of Cerberus by implementing it in an existing enclave platform, RISC-V Keystone.
△ Less
Submitted 14 November, 2022; v1 submitted 30 September, 2022;
originally announced September 2022.
-
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Authors:
Elizabeth Polgreen,
Kevin Cheang,
Pranav Gaddamadugu,
Adwait Godbole,
Kevin Laeufer,
Shaokai Lin,
Yatin A. Manerkar,
Federico Mora,
Sanjit A. Seshia
Abstract:
UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combinations of hardware and software, or those that have multiple, varied specifications, or systems that require hybrid modes of modeling. A novel aspect of \uclid is an emphasis on the use of syntax-guided and inductive sy…
▽ More
UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combinations of hardware and software, or those that have multiple, varied specifications, or systems that require hybrid modes of modeling. A novel aspect of \uclid is an emphasis on the use of syntax-guided and inductive synthesis to automate steps in modeling and verification. This tool paper presents new developments in the \uclid tool including new language features, integration with new techniques for syntax-guided synthesis and satisfiability solving, support for hyperproperties and combinations of axiomatic and operational modeling, demonstrations on new problem classes, and a robust implementation.
△ Less
Submitted 7 August, 2022;
originally announced August 2022.
-
Synthesis in Uclid5
Authors:
Federico Mora,
Kevin Cheang,
Elizabeth Polgreen,
Sanjit A. Seshia
Abstract:
We describe an integration of program synthesis into Uclid5, a formal modelling and verification tool. To the best of our knowledge, the new version of Uclid5 is the only tool that supports program synthesis with bounded model checking, k-induction, sequential program verification, and hyperproperty verification. We use the integration to generate 25 program synthesis benchmarks with simple, known…
▽ More
We describe an integration of program synthesis into Uclid5, a formal modelling and verification tool. To the best of our knowledge, the new version of Uclid5 is the only tool that supports program synthesis with bounded model checking, k-induction, sequential program verification, and hyperproperty verification. We use the integration to generate 25 program synthesis benchmarks with simple, known solutions that are out of reach of current synthesis engines, and we release the benchmarks to the community.
△ Less
Submitted 16 July, 2020; v1 submitted 13 July, 2020;
originally announced July 2020.
-
Using Convolutional Neural Networks to Count Palm Trees in Satellite Images
Authors:
Eu Koon Cheang,
Teik Koon Cheang,
Yong Haur Tay
Abstract:
In this paper we propose a supervised learning system for counting and localizing palm trees in high-resolution, panchromatic satellite imagery (40cm/pixel to 1.5m/pixel). A convolutional neural network classifier trained on a set of palm and no-palm images is applied across a satellite image scene in a sliding window fashion. The resultant confidence map is smoothed with a uniform filter. A non-m…
▽ More
In this paper we propose a supervised learning system for counting and localizing palm trees in high-resolution, panchromatic satellite imagery (40cm/pixel to 1.5m/pixel). A convolutional neural network classifier trained on a set of palm and no-palm images is applied across a satellite image scene in a sliding window fashion. The resultant confidence map is smoothed with a uniform filter. A non-maximal suppression is applied onto the smoothed confidence map to obtain peaks. Trained with a small dataset of 500 images of size 40x40 cropped from satellite images, the system manages to achieve a tree count accuracy of over 99%.
△ Less
Submitted 23 January, 2017;
originally announced January 2017.
-
Segmentation-free Vehicle License Plate Recognition using ConvNet-RNN
Authors:
Teik Koon Cheang,
Yong Shean Chong,
Yong Haur Tay
Abstract:
While vehicle license plate recognition (VLPR) is usually done with a sliding window approach, it can have limited performance on datasets with characters that are of variable width. This can be solved by hand-crafting algorithms to prescale the characters. While this approach can work fairly well, the recognizer is only aware of the pixels within each detector window, and fails to account for oth…
▽ More
While vehicle license plate recognition (VLPR) is usually done with a sliding window approach, it can have limited performance on datasets with characters that are of variable width. This can be solved by hand-crafting algorithms to prescale the characters. While this approach can work fairly well, the recognizer is only aware of the pixels within each detector window, and fails to account for other contextual information that might be present in other parts of the image. A sliding window approach also requires training data in the form of presegmented characters, which can be more difficult to obtain. In this paper, we propose a unified ConvNet-RNN model to recognize real-world captured license plate photographs. By using a Convolutional Neural Network (ConvNet) to perform feature extraction and using a Recurrent Neural Network (RNN) for sequencing, we address the problem of sliding window approaches being unable to access the context of the entire image by feeding the entire image as input to the ConvNet. This has the added benefit of being able to perform end-to-end training of the entire model on labelled, full license plate images. Experimental results comparing the ConvNet-RNN architecture to a sliding window-based approach shows that the ConvNet-RNN architecture performs significantly better.
△ Less
Submitted 23 January, 2017;
originally announced January 2017.
