All Publications
# VST
# Iris
# Weak Memory
Ongoing Projects
  • VST and concurrency: Extend VST's soundness proof and logic to support concurrency, atomic operations, and weak memory
  • RefinedVST: Build an annotation-based proof tool on top of VST using the RefinedC framework
Past Projects
  • Verification of Concurrent C Programs with Search Structure Templates
  • Developing specifications for Relaxed libraries, built on top of Iris
(for publications)

2024

Compositional Verification of Concurrent C Programs with Search Structure Templates

Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang

CPP (ACM SIGPLAN International Conference on Certified Programs and Proofs) 2024

Concurrent search structure templates are a technique for separating the verification of a concurrent data structure into concurrency-control and data-structure components, which can then be modularly combined with no additional proof effort. In this paper, we implement the template approach in the Verified Software Toolchain (VST), and use it to prove correctness of C implementations of fine-grained concurrent data structures. This involves translating code, specifications, and proofs to the idiom of C and VST, and gives us another look at the requirements and limitations of the template approach. We encounter several questions about the boundaries between template and data structure, as well as some common data structure operations that cannot naturally be decomposed into templates. Nonetheless, the approach appears promising for modular verification of real-world concurrent data structures.

# VST # Iris

Compositional Verification of Concurrent C Programs with Search Structure Templates

Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang

CPP (ACM SIGPLAN International Conference on Certified Programs and Proofs) 2024

Concurrent search structure templates are a technique for separating the verification of a concurrent data structure into concurrency-control and data-structure components, which can then be modularly combined with no additional proof effort. In this paper, we implement the template approach in the Verified Software Toolchain (VST), and use it to prove correctness of C implementations of fine-grained concurrent data structures. This involves translating code, specifications, and proofs to the idiom of C and VST, and gives us another look at the requirements and limitations of the template approach. We encounter several questions about the boundaries between template and data structure, as well as some common data structure operations that cannot naturally be decomposed into templates. Nonetheless, the approach appears promising for modular verification of real-world concurrent data structures.

2022

Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic

Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer

PLDI 2022 (ACM SIGPLAN Conference on Programming Languages Design and Implementation)

Several functional correctness criteria have been proposed for relaxed-memory consistency libraries, but most lack support for modular client reasoning. Mével and Jourdan recently showed that logical atomicity can be used to give strong modular Hoare-style specifications for relaxed libraries, but only for a limited instance in the Multicore OCaml memory model. It has remained unclear if their approach scales to weaker implementations in weaker memory models. In this work, we combine logical atomicity together with richer partial orders (inspired by prior relaxed-memory correctness criteria) to develop stronger specifications in the weaker memory model of Repaired C11 (RC11). We show their applicability by proving them for multiple implementations of stacks, queues, and exchangers, and we demonstrate their strength by performing multiple client verifications on top of them. Our proofs are mechanized in COMPASS, a new framework extending the iRC11 separation logic, built atop Iris, in Coq. We report the first mechanized verifications of relaxed-memory implementations for the exchanger, the elimination stack, and the Herlihy-Wing queue.

#wm # iris

Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic

Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer

PLDI 2022 (ACM SIGPLAN Conference on Programming Languages Design and Implementation)

Several functional correctness criteria have been proposed for relaxed-memory consistency libraries, but most lack support for modular client reasoning. Mével and Jourdan recently showed that logical atomicity can be used to give strong modular Hoare-style specifications for relaxed libraries, but only for a limited instance in the Multicore OCaml memory model. It has remained unclear if their approach scales to weaker implementations in weaker memory models. In this work, we combine logical atomicity together with richer partial orders (inspired by prior relaxed-memory correctness criteria) to develop stronger specifications in the weaker memory model of Repaired C11 (RC11). We show their applicability by proving them for multiple implementations of stacks, queues, and exchangers, and we demonstrate their strength by performing multiple client verifications on top of them. Our proofs are mechanized in COMPASS, a new framework extending the iRC11 separation logic, built atop Iris, in Coq. We report the first mechanized verifications of relaxed-memory implementations for the exchanger, the elimination stack, and the Herlihy-Wing queue.

2021

Foundations for Reasoning about Holistic Specifications
Foundations for Reasoning about Holistic Specifications

Duc Than Nguyen

Master of Philosophy - Dissertation @ University of Melbourne, Australia

Specifications of sufficient conditions may be enough for reasoning about complete and unchanging programs of a closed system. Nevertheless, there is no luxury of trusting external components of probably unknown provenance in an open world that may be buggy or potentially malicious. It is critical to ensure that our components are robust when cooperating with a wide variety of external components. Holistic specifications, which are concerned with sufficient and necessary conditions, could make programs more robust in an open-world setting. In this thesis, we lay the foundations for reasoning about holistic specifications. We give an Isabelle/HOL mechanization of holistic specifications focusing on object-based programs. We also pave a way to reason about holistic specifications via proving some key lemmas that we hope will be useful in the future to establish a general logic for holistic specifications.

Foundations for Reasoning about Holistic Specifications

Duc Than Nguyen

Master of Philosophy - Dissertation @ University of Melbourne, Australia

Specifications of sufficient conditions may be enough for reasoning about complete and unchanging programs of a closed system. Nevertheless, there is no luxury of trusting external components of probably unknown provenance in an open world that may be buggy or potentially malicious. It is critical to ensure that our components are robust when cooperating with a wide variety of external components. Holistic specifications, which are concerned with sufficient and necessary conditions, could make programs more robust in an open-world setting. In this thesis, we lay the foundations for reasoning about holistic specifications. We give an Isabelle/HOL mechanization of holistic specifications focusing on object-based programs. We also pave a way to reason about holistic specifications via proving some key lemmas that we hope will be useful in the future to establish a general logic for holistic specifications.

2015

Efficient Privacy Preserving Data Audit in Cloud
Efficient Privacy Preserving Data Audit in Cloud

Hai-Van Dang, Thai-Son Tran, Duc-Than Nguyen, Thach V. Bui, Dinh-Thuc Nguyen

Advanced Computational Methods for Knowledge Engineering 2015

With the development of database-as-a-service (DaS), data in cloud is more interesting for researchers in both academia and commercial societies. Despite DaS’s convenience, there exist many considerable problems which concern end users about data loss and malicious deletion. In order to avoid these cases, users can rely on data auditing, which means verifying the existence of data stored in cloud without any malicious changes. Data owner can perform data auditing by itself or hire a third-party auditor. Until now, there are two challenges of data auditing as the computation cost in case of self auditing and data privacy preservation in case of hiding an auditor. In this paper, we propose a solution for auditing by a third-party auditor to verify data integrity with efficient computation and data privacy preservation. Our solution is built upon cryptographic hash function and Chinese Theorem Remainder with the advantage in efficient computation in all three sides including data owner, cloud server, and auditor. In addition, the privacy preservation can be guaranteed by proving the third-party auditor learns nothing about user’s data during auditing process.

Efficient Privacy Preserving Data Audit in Cloud

Hai-Van Dang, Thai-Son Tran, Duc-Than Nguyen, Thach V. Bui, Dinh-Thuc Nguyen

Advanced Computational Methods for Knowledge Engineering 2015

With the development of database-as-a-service (DaS), data in cloud is more interesting for researchers in both academia and commercial societies. Despite DaS’s convenience, there exist many considerable problems which concern end users about data loss and malicious deletion. In order to avoid these cases, users can rely on data auditing, which means verifying the existence of data stored in cloud without any malicious changes. Data owner can perform data auditing by itself or hire a third-party auditor. Until now, there are two challenges of data auditing as the computation cost in case of self auditing and data privacy preservation in case of hiding an auditor. In this paper, we propose a solution for auditing by a third-party auditor to verify data integrity with efficient computation and data privacy preservation. Our solution is built upon cryptographic hash function and Chinese Theorem Remainder with the advantage in efficient computation in all three sides including data owner, cloud server, and auditor. In addition, the privacy preservation can be guaranteed by proving the third-party auditor learns nothing about user’s data during auditing process.

2013

Attacks on Low Private Exponent RSA: An Experimental Study
Attacks on Low Private Exponent RSA: An Experimental Study

Nguyen, Thuc D., Than Duc Nguyen, Long D. Tran

International Conference on Computational Science and Its Applications 2013

RSA cryptosystem is the most popular public key cryptosystem which provides both secrecy and digital signatures. Due to RSA’s popularity, many attacks on it have been developed. In this paper, we consider experimentally attacks on low private exponent RSA and find that: (i) lattice attack using Gauss lattice reduction algorithm is more effective than Wiener attack, and (ii) it is not always to recover decryption exponent even if its bit-length is less than onequarter bit-length of the modulus. The results also raise an open question on the conditions to recover the RSA private key from public key.

Attacks on Low Private Exponent RSA: An Experimental Study

Nguyen, Thuc D., Than Duc Nguyen, Long D. Tran

International Conference on Computational Science and Its Applications 2013

RSA cryptosystem is the most popular public key cryptosystem which provides both secrecy and digital signatures. Due to RSA’s popularity, many attacks on it have been developed. In this paper, we consider experimentally attacks on low private exponent RSA and find that: (i) lattice attack using Gauss lattice reduction algorithm is more effective than Wiener attack, and (ii) it is not always to recover decryption exponent even if its bit-length is less than onequarter bit-length of the modulus. The results also raise an open question on the conditions to recover the RSA private key from public key.