GREGORY J. DUCK

Gregory J. Duck
Research Assistant Professor
National University of Singapore
Office: COM2-03-33
Email:

Gregory is a Research Assistant Professor at the National University of Singapore.

Previously, Gregory received his BSc (Mathematics), BEng (Software) and Phd (Computer Science) from the University of Melbourne. From 2011 Gregory works at the National University of Singapore.

Gregory's research interests include: systems, security, binary rewriting, fuzzing, repair, and programming languages.

• EnvFuzz: A binary fuzzer that can fuzz just about anything (GUI/network/editors/compilers/etc.)
• BlueFat: Strong and compatible memory safety with Fully Randomized Pointers (FRP).
• RedFat: A binary hardening system for the x86_64.
  • libredfat: A hardened malloc() replacement.
• E9Patch: A powerful static binary rewriter.
  
  • E9Syscall: System call hooking using static binary rewriting.
  • E9AFL: Binary fuzzing using AFL.
• EffectiveSan: Type and memory error detection using dynamically typed C/C++
• LowFat - Lean program hardening with low-fat pointers.

Publications:

• Ruijie Meng, Gregory J. Duck, Abhik Roychoudhury, Program Environment Fuzzing, Computer and Communications Security (CCS), 2024, [github] [abstract]

  Abstract:
  Computer programs are not executed in isolation, but rather interact with the execution environment which drives the program behaviors. Software validation methods thus need to capture the effect of possibly complex environmental interactions. Program environments may come from files, databases, configurations, network sockets, human-user interactions, and more. Conventional approaches for environment capture in symbolic execution and model checking employ environment modeling, which involves manual effort. In this paper, we take a different approach based on an extension of greybox fuzzing. Given a program, we first record all observed environmental interactions at the kernel/usermode boundary in the form of system calls. Next, we replay the program under the original recorded interactions, but this time with selective mutations applied, in order to get the effect of different program environments—all without environment modeling. Via repeated (feedback-driven) mutations over a fuzzing campaign, we can search for program environments that induce crashing behaviors. Our EnvFuzz tool found 33 previously unknown bugs in well-known real-world protocol implementations and GUI applications. Many of these are security vulnerabilities and 16 CVEs were assigned.

• Dylan Wolff, Shi Zheng, Gregory J. Duck, Umang Mathur, Abhik Roychoudhury, Greybox Fuzzing for Concurrency Testing, Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2024
• Ridwan Shariffdeen, Yannic Noller, Martin Mirchev, Haifeng Ruan, Xiang Gao, Andreea Costea, Gregory J. Duck, Abhik Roychoudhury, Program Repair Competition 2024, Workshop on Automated Program Repair (APR), 2024
• Jinsheng Ba, Gregory J. Duck, Abhik Roychoudhury, Efficient Greybox Fuzzing to Detect Memory Errors, Automated Software Engineering (ASE), 2022 [github]
  ★ ACM SIGSOFT Distinguished Paper Award ★
• Yuancheng Jiang, Gregory J. Duck, Roland H. C. Yap, Zhenkai Liang, Pinghai Yuan, Extensible Virtual Call Integrity, European Symposium on Research in Computer Security (ESORICS), 2022
• Yuntong Zhang, Xiang Gao, Gregory J. Duck, Abhik Roychoudhury, Program Vulnerability Repair via Inductive Inference, International Symposium on Software Testing and Analysis (ISSTA), 2022 [github]
• Gregory J. Duck, Yuntong Zhang, Roland H. C. Yap, Hardening Binaries against More Memory Errors, European Conference on Computer Systems (EuroSys), 2022 [github] [download] [abstract]

  Abstract:
  Memory errors, such as buffer overflows and use-after-free, remain the root cause of many security vulnerabilities in modern software. The use of closed source software further exacerbates the problem, as source-based memory error mitigation cannot be applied. While many memory error detection tools exist, most are based on a single error detection methodology with resulting known limitations, such as incomplete memory error detection (redzones) or false error detections (low-fat pointers). In this paper we introduce RedFat, a memory error hardening tool for stripped binaries that is fast, practical and scalable. The core idea behind RedFat is to combine complementary error detection methodologies---redzones and low-fat pointers---in order to detect more memory errors that can be detected by each individual methodology alone. However, complementary error detection also inherits the limitations of each approach, such as false error detections from low-fat pointers. To mitigate this, we introduce a profile-based analysis that automatically determines the strongest memory error protection possible without negative side effects.

  We implement RedFat on top of a scalable binary rewriting framework, and demonstrate low overheads compared to the current state-of-the-art. We show RedFat to be language agnostic on C/C++/Fortran binaries with minimal requirements, and works with stripped binaries for both position independent/dependent code. We also show that the RedFat instrumentation can scale to very large/complex binaries, such as Google Chrome.

• Xiang Gao, Gregory J. Duck, Abhik Roychoudhury, Scalable Fuzzing of Program Binaries with E9AFL, Automated Software Engineering (ASE), 2021 [tool paper] [github] [download] [abstract]

  Abstract:
  Greybox fuzzing is an effective method for software testing. Greybox fuzzers, such as AFL, use instrumentation that collects path coverage information in order to guide the fuzzing process. The instrumentation is usually inserted by a modified compiler toolchain, meaning that the program must be recompiled in order to be compatible with greybox fuzzing. When source code is unavailable, or for projects with complex build systems, recompilation is not always feasible. In this paper, we present E9AFL, a fast and scalable tool that automatically inserts AFL instrumentation to program binaries. E9AFL is built on top of the E9Patch static binary rewriting tool. To combat the overhead caused by binary instrumentation, E9AFL develops a set of optimization strategies. Our evaluation results show that E9AFL outperforms existing binary instrumentation tools and achieves comparable performance with the compile time instrumentation.

• Ridwan Shariffdeen, Xiang Gao, Gregory J. Duck, Shin Hwei Tan, Julia Lawall, Abhik Roychoudhury, Automated Patch Backporting in Linux (Experience Paper), International Symposium on Software Testing and Analysis (ISSTA), 2021 [github]
  ★ ISSTA 2021 Distingluished Artifact Award ★
• Xiang Gao, Bo Wang, Gregory J. Duck, Ruyi Ji, Yingfei Xiong, Abhik Roychoudhury, Beyond Tests: Program Vulnerability Repair via Crash Constraint Extraction, Transactions on Software Engineering and Methodology (TOSEM), 2021
• Gregory J. Duck, Xiang Gao, Abhik Roychoudhury, Binary Rewriting without Control Flow Recovery, Programming Language Design and Implementation (PLDI), 2020 [github] [download] [abstract]

  Abstract:
  Static binary rewriting has many important applications in software security and systems, such as hardening, repair, patching, instrumentation, and debugging. While many different static binary rewriting tools have been proposed, most rely on recovering control flow information from the input binary. The recovery step is necessary since the rewriting process may move instructions, meaning that the set of jump targets in the rewritten binary needs to be adjusted accordingly. Since the static recovery of control flow information is a hard problem in general, most tools rely on a set of simplifying heuristics or assumptions, such as specific compilers, specific source languages, or binary file meta information. However, the reliance on assumptions or heuristics tends to scale poorly in practice, and most state-of-the-art static binary rewriting tools cannot handle very large/complex programs such as web browsers.

  In this paper we present E9Patch, a tool that can statically rewrite x86_64 binaries without any knowledge of control flow information. To do so, E9Patch develops a suite of binary rewriting methodologies---such as instruction punning, padding, and eviction---that can insert jumps to trampolines without the need to move other instructions. Since this preserves the set of jump targets, the need for control flow recovery and related heuristics is eliminated. As such, E9Patch is robust by design, and can scale to very large (>100MB) stripped binaries including the Google Chrome and FireFox web browsers. We also evaluate the effectiveness of E9Patch against realistic applications such as binary instrumentation, hardening and repair.

• Gregory J. Duck, Joxan Jaffar, and Roland H. C. Yap, Shape Neutral Analysis of Graph-based Data-structures, International Conference on Logic Programming (ICLP), Theory and Practice of Logic Programming (TPLP), 2018, [abstract]

  Abstract:
  Malformed data-structures can lead to runtime errors such as arbitrary memory access or corruption. Despite this, reasoning over data-structure properties for low-level heap manipulating programs remains challenging. In this paper we present a constraint-based program analysis that checks data-structure integrity, w.r.t. given target data-structure properties, as the heap is manipulated by the program. Our approach is to automatically generate a solver for properties using the type definitions from the target program. The generated solver is implemented using a Constraint Handling Rules (CHR) extension of built-in heap, integer and equality solvers. A key property of our program analysis is that the target data-structure properties are shape neutral, i.e., the analysis does not check for properties relating to a given data-structure graph shape, such as doubly-linked-lists versus trees. Nevertheless, the analysis can detect errors in a wide range of data-structure manipulating programs, including those that use lists, trees, DAGs, graphs, etc. We present an implementation that uses the Satisfiability Modulo Constraint Handling Rules (SMCHR) system. Experimental results show that our approach works well for real-world C programs.

• Gregory J. Duck, Roland H. C. Yap, EffectiveSan: Type and Memory Error Detection using Dynamically Typed C/C++, Programming Language Design and Implementation (PLDI), 2018, [github] [download] [abstract]

  Abstract:
  Low-level programming languages with weak/static type systems, such as C and C++, are vulnerable to errors relating to the misuse of memory at runtime, such as (sub-)object bounds overflows, (re)use-after-free, and type confusion. Such errors account for many security and other undefined behavior bugs for programs written in these languages. In this paper, we introduce the notion of dynamically typed C/C++, which aims to detect such errors by dynamically checking the "effective" type of each object before use at runtime. We also present an implementation of dynamically typed C/C++ in the form of the Effective Type Sanitizer (EffectiveSan). EffectiveSan enforces type and memory safety using a combination of low-fat pointers, type meta data and type/bounds check instrumentation. We evaluate EffectiveSan against the SPEC2006 benchmark suite and the Firefox web browser, and detect several new type and memory errors. We also show that EffectiveSan achieves high compatibility and reasonable overheads for the given error coverage. Finally, we highlight that EffectiveSan is one of only a few tools that can detect sub-object bounds errors, and uses a novel approach (dynamic type checking) to do so.

• Gregory J. Duck, Roland H. C. Yap, Lorenzo Cavallaro, Stack Bounds Protection with Low Fat Pointers, Network and Distributed System Security Symposium (NDSS), 2017 [github] [abstract]

  Abstract:
  Object bounds overflow errors are a common source of security vulnerabilities. In principle, bounds check instrumentation eliminates the problem, but is hampered by limited compatibility against un-instrumented code and high overheads. On 64-bit systems, low-fat pointers are a recent scheme for implementing efficient and compatible bounds checking by transparently encoding meta information within the native pointer representation itself. However, low-fat pointers are traditionally used for heap objects only, where the allocator has sufficient control over object location necessary for the encoding. This is a problem for stack allocation, where there exist strong constraints regarding the location of stack objects that is apparently incompatible with low-fat pointers. In this paper, we present an extension of low-fat pointers to stack objects by using a collection of techniques, such as pointer mirroring and memory aliasing, thereby allowing stack objects to enjoy bounds error protection from instrumented code. Our extension is compatible with common special uses of the stack, such as alloca, setjmp and longjmp, exceptions, and multi-threading, which rely on direct manipulation of the stack pointer. Our experiments show that we successfully extend the advantages of the low-fat pointer encoding to stack objects. The end result is competitive bounds checking instrumentation for the stack and heap with low memory and runtime overheads, and high compatibility with un-instrumented legacy code.

• Gregory J. Duck, Roland H. C. Yap, Heap Bounds Protection with Low Fat Pointers, Compiler Construction (CC), 2016 [github] [abstract]

  Abstract:
  Heap buffer overflow (underflow) errors are a common source of security vulnerabilities. One prevention mechanism is to add object bounds meta information and to instrument the program with explicit bounds checks for all memory access. The so-called fat pointers approach is one method for maintaining and propagating the meta information where native machine pointers are replaced with fat objects that explicitly store object bounds. Another approach is low fat pointers, which encodes meta information within a native pointer itself, eliminating space overheads and also code compatibility issues. This paper presents a new low fat pointer encoding that is fully compatible with existing libraries (e.g. pre-compiled libraries unaware of the encoding) and standard hardware (e.g. x86_64). We show that our approach has very low memory overhead, and competitive with existing state-of-the-art bounds instrumentation solutions.

• Gregory J. Duck, Rémy Haemmerlé and Martin Sulzmann, On Termination, Confluence and Consistent CHR-based Type Inference, International Conference on Logic Programming (ICLP), Theory and Practice of Logic Programming (TPLP), 2014 [abstract]

  Abstract:
  We consider the application of Constraint Handling Rules (CHR) for the specification of type inference systems, such as that used by Haskell. Confluence of CHR guarantees that the answer provided by type inference is correct and consistent. The standard method for establishing confluence relies on an assumption that the CHR program is terminating. However, many examples in practice give rise to non-terminating CHR programs, rendering this method inapplicable. Despite no guarantee of termination or confluence, the Glasgow Haskell Compiler (GHC) supports options that allow the user to proceed with type inference anyway, e.g. via the use of the UndecidableInstances flag. In this paper we formally identify and verify a set of relaxed criteria, namely range-restrictedness, local confluence, and ground termination, that ensure the consistency of CHR-based type inference that maps to potentially non-terminating CHR programs.

• Gregory J. Duck, Joxan Jaffar, Nicolas C. H. Koh, Constraint-based Program Reasoning with Heaps and Separation, Constraint Programming (CP), 2013 [github] [abstract]

  Abstract:
  This paper introduces a constraint language H for finite partial maps (a.k.a. heaps) that incorporates the notion of separation from Separation Logic. We use H to build an extension of Hoare Logic for reasoning over heap manipulating programs using (constraint-based) symbolic execution. We present a sound and complete algorithm for solving quantifier-free (QF) H-formulae based on heap element propagation. An implementation of the H-solver has been integrated into a Satisfiability Modulo Theories (SMT) framework. We experimentally evaluate the implementation against Verification Conditions (VCs) generated from symbolic execution of large (heap manipulating) programs. In particular, we mitigate the path explosion problem using subsumption via interpolation -- made possible by the constraint-based encoding.

• Gregory J. Duck, Satisfiability Modulo Constraint Handling Rules (Extended Abstract), International Joint Conference on Artificial Intelligence (IJCAI), 2013 [github] [abstract]

  Abstract:
  Satisfiability Modulo Constraint Handling Rules (SMCHR) is the integration of the Constraint Handling Rules (CHRs) solver programming language into a Satisfiability Modulo Theories (SMT) solver framework. Constraint solvers are implemented in CHR as a set of high-level rules that specify the simplification (rewriting) and constraint propagation behaviour. The traditional CHR execution algorithm manipulates a global store representing a flat conjunction of constraints. This paper introduces SMCHR: a tight integration of CHR with a modern Boolean Satisfiability (SAT) solver. Unlike CHR, SMCHR can handle (quantifier-free) formulae with an arbitrary propositional structure. SMCHR is essentially a Satisfiability Modulo Theories (SMT) solver where the theory T is implemented in CHR.

• Gregory J. Duck, SMCHR: Satisfiability Modulo Constraint Handling Rules, International Conference on Logic Programming (ICLP), Theory and Practice of Logic Programming (TPLP), 2012. [github] [abstract]
  ★ ICLP 2012 Best Paper Award ★
  

  Abstract:
  Constraint Handling Rules (CHRs) are a high-level rule-based programming language for specification and implementation of constraint solvers. CHR manipulates a global store representing a flat conjunction of constraints. By default, CHR does not support goals with a more complex propositional structure including disjunction, negation, etc., or CHR relies on the host system to provide such features. In this paper we introduce Satisfiability Modulo Constraint Handling Rules (SMCHR): a tight integration of CHR with a modern Boolean Satisfiability (SAT) solver for quantifier-free formulae with an arbitrary propositional structure. SMCHR is essentially a Satisfiability Modulo Theories (SMT) solver where the theory T is implemented in CHR. The execution algorithm of SMCHR is based on lazy clause generation, where a new clause for the SAT solver is generated whenever a rule is applied. We shall also explore the practical aspects of building an SMCHR system, including extending a "built-in" constraint solver supporting equality with unification and justifications.

• Leslie De Koninck, Gregory J. Duck, and Peter J. Stuckey. Demand-driven normalisation for ACD term rewriting, International Conference on Logic Programming (ICLP), 2009.
• Gregory J. Duck, Peter J. Stuckey, Leslie De Koninck, Cadmium: An Implementation of ACD Term Rewriting, International Conference on Logic Programming (ICLP), 2008. [github]
• Leslie De Koninck, Peter J. Stuckey, and Gregory J. Duck, Optimizing compilation of CHR with rule priorities, Symposium on Functional and Logic Programming (FLOPS), 2008.
• Sebastian Brand, Gregory J. Duck, Jakob Puchinger, and Peter J. Stuckey, Flexible, Rule-based Constraint Model Linearisation, Practical Aspects of Declarative Languages (PADL), 2008.
• Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones, Peter J. Stuckey, Understanding Functional Dependencies via Constraint Handling Rules, Journal of Functional Programming, 2007.
• Gregory J. Duck, Peter J. Stuckey, and Martin Sulzmann, Observable Confluence for Constraint Handling Rules, International Conference on Logic Programming (ICLP), 2007.
• Nicholas Nethercote, Peter J. Stuckey, Ralph Becket, Sebastian Brand, Gregory J. Duck and Guido Tack. MiniZinc: Towards a Standard CP Modelling Language, Constraint Programming (CP), 2007.
• Tom Schrijvers, Bart Demoen, Gregory J. Duck, Peter J. Stuckey, Thom W. Frühwirth, Automatic Implication Checking for CHR Constraints, Electronic Notes in Theoretical Computer Science, 2006
• Gregory J. Duck, Peter J. Stuckey, Sebastian Brand, ACD Term Rewriting, International Conference on Logic Programming (ICLP), 2006. [github]
• Gregory J. Duck, Compilation of Constraint Handling Rules, 2005. [PhD thesis]
• Tom Schrijvers, Peter J. Stuckey, Gregory J. Duck, Abstract Interpretation for Constraint Handling Rules, Principles and Practice of Declarative Programming (PPDP), 2005
• Christian Holzbaur, Maria Garcia de la Banda, Peter J. Stuckey, and Gregory J. Duck. Optimizing Compilation of Constraint Handling Rules in HAL, Special Issue of Theory and Practice of Logic Programming on Constraint Handling Rules, 2004.
• Gregory J. Duck, Maria Garcia de la Banda, Peter J. Stuckey. Compiling Ask Constraints, International Conference on Logic Programming (ICLP), 2004.
• Gregory J. Duck, Peter J. Stuckey, Maria Garcia de la Banda, Christian Holzbaur. The Refined Operational Semantics of Constraint Handling Rules, International Conference on Logic Programming (ICLP), 2004.
  ★ ICLP 2014 Test of Time Award (10 Years) ★
• Gregory J. Duck, Simon Peyton Jones, Peter J. Stuckey, and Martin Sulzmann. Sound and Decidable Type Inference for Functional Dependencies, European Symposium on Programming (ESOP), 2004.
• Gregory J. Duck, Peter J. Stuckey, Maria Garcia de la Banda, and Christian Holzbaur. Extending Arbitrary Solvers with Constraint Handling Rules, Principles and Practice of Declarative Programming (PPDP), 2003.

Other:

• Gregory J. Duck, Sai Dhawal Phaye, Roland H. C. Yap, Trevor E. Carlson, Fully Randomized Pointers, 2024, [preprint] [github]
• Gregory J. Duck, Roland H. C. Yap, An Extended Low Fat Allocator API and Applications, Technical Report, 2018. [github]
• Ralph Becket, Sebastian Brand, Mark Brown, Gregory J. Duck, Thibaut Feydy, Julien Fischer, Jinbo Huang, Kim Marriott, Nicholas Nethercote, Jakob Puchinger, Reza Rafeh, Peter J. Stuckey, and Mark G. Wallace, The Many Roads Leading to Rome: Solving Zinc Models by Various Solvers, Workshop on Constraint Modelling and Reformulation (ModRef), 2008.
• Sebastian Brand, Gregory J. Duck, Jakob Puchinger, and Peter J. Stuckey, A Rule-based System for Model Transformation, Workshop on Constraint Modelling and Reformulation (ModRef), 2007.
• Gregory J. Duck, Peter J. Stuckey, Martin Sulzmann, Observable Confluence for Constraint Handling Rules, Workshop on Constraint Handling Rules, 2006.
• Gregory J. Duck, Tom Schrijvers, Accurate Functional Dependency Analysis for Constraint Handling Rules, Workshop on Constraint Handling Rules, 2005.
• Tom Schrijvers, Bart Demoen, Gregory J. Duck, Peter J. Stuckey, and Thom Frühwirth, Automatic implication checking for CHR constraints, Workshop on Rule-Based Programming, 2005.