TestGenerator

---

DNS Nameserver Tests -   Valid Zone File Tests   ·   Invalid Zone File Tests     |     Pre-generated Tests     |     Installation     |     Generation of Tests

---

DNS Nameserver Tests

A test case in DNS consists of a query and zone file.

Valid Zone File Tests

Ferret generates valid tests, where each valid test consists of a valid zone file and a valid query by executing the Zen model of the authoritative semantics of DNS present in this folder, which is based on the DNS formal semantics that we developed from multiple DNS RFCs. Our formal semantics focuses on query lookup at a single nameserver, which we model as a stateless function that takes a user query and a zone file and produces a DNS response. The figure below shows an abstract view of this function as a decision tree. Each leaf node represents a unique case in the DNS, where a response is created and returned to the user.

_{[ Abstract representation of the Authoritative DNS decision tree used to respond to a user query. ]}

Symbolic execution of the above function (tree) generates inputs that drive the function down different execution paths, enabling Ferret to explore the space of DNS behaviors and feature interactions systematically.

Invalid Zone File Tests

While it’s critical to be able to generate well-formed zone files for testing, bugs can also lurk in implementations' handling of ill-formed zones. Our executable Zen model includes a formulation of the validity conditions for zone files.

CLICK to reveal zone validity conditions

---

	Validity Condition	RFC Document
i.	All records should be unique (there should be no duplicates).	2181
ii.	A zone file should contain exactly one SOA record.	1035
iii.	The zone domain should be prefix to all the resource records domain name.	1034
iv.	If there is a CNAME type then no other type can exist and only one CNAME can exist for a domain name.	1034
v.	There can be only one DNAME record for a domain name.	6672
vi.	A domain name cannot have both DNAME and NS records unless there is an SOA record as well.	6672
vii.	No DNAME record domain name can be a prefix of another record’s domain name.	6672
viii.	No NS record can have a non-SOA domain name that is a prefix of another NS record.	1034
ix.	Glue records must exist for all NS records in a zone.	1035

---

Ferret leverages Zen to generate zone files that violate one of these conditions systematically. The formal model shown in the earlier image is well defined only for valid zone files, and therefore, we use GRoot to generate queries for these invalid zone files.

Pre-generated Tests

Ferret takes in the maximum length of the domain name and the maximum number of records in the zone as an integer from the user. The tests generated for a given maximum bound is constant and do not change with each run. Therefore, we have released the tests generated for a maximum bound of 4 in a separate GitHub repository - FerretDataset.

The dataset consists of both valid and invalid zone file tests. For valid zone files, the 12,673 tests in the valid zone file tests folder are exhaustive i.e., there is a test for each possible path of the model for that bound. For the invalid zone file tests, we have generated 900 ill-formed zone files, 100 violating each of the validity conditions.

Note: Use the tests in the FerretDataset that were generated with the maximum bound of 4 to skip this module to save time and go directly to the Differential testing module. For other bounds, please follow the installation and test generation steps.

Installation

Native Installation

0. Install dotnet-sdk-5.0 for your OS.
1. Build the project using^# (from TestGenerator directory):

   ~/TestGenerator$ dotnet build --configuration Release

^# Alternatively, you could open the solution in Visual Studio in Windows and build using it.

Using docker

Note: The docker image may consume ~ 2 GB of disk space.

If you have trouble with native installation, then using docker is recommend as they have negligible performance overhead. (See this report)

0. Get docker for your OS.

1. Build the docker image locally (from TestGenerator directory):

   ~/TestGenerator$ docker build -t ferrettestgen .

2. Run a container over the image using: docker run -it --name=testgen ferrettestgen.
   This would give you a bash shell within the container's TestGenerator directory.

Generation of Tests

1. If a docker container will be used for the test generation, either

   • Copy the Results folder from the docker container to the host system after running the tool using the following command from the host terminal.

     ~/TestGenerator$ docker cp testgen:/home/ferret/Ferret/TestGenerator/Results .

   • Or first create a Results folder in the host system and bind mount it while running the container:

     ~/TestGenerator$ docker run -v ${PWD}/Results:/home/ferret/Ferret/TestGenerator/Results -it --name=testgen ferrettestgen

     This would give you a bash shell within the container's TestGenerator directory.

2. Run using:

   ~/TestGenerator$ dotnet run --configuration Release --project Samples

   CLICK to show all command-line options

    -o, --outputDir    (Default: Results/) The path to the folder to output the generated tests.
   
    -f, --function     (Default: RRLookup) Generate tests for either RRLookup (1) or generate invalid zone files InvalidZoneFiles (2).
   
    -l, --length       (Default: 4) The maximum number of records in a zone and the maximum length of a domain.
   
    --help             Display this help screen.
   
    --version          Display version information. 

   • Pass the option using dotnet run --configuration Release --project Samples -- -l 3.
   • The RRLookup function generates valid tests which are a pair of zone and query.
   • The InvalidZoneFiles function generates invalid zone files by negating one validity constraint at a time while keeping the others true. For each negated constraint, the tool tries to generates 100 zone files.

3. Est. Time:

   • Ferret takes approximately 6 hours for RRLookup with a maximum bound of 4 to generate 12,673 tests. Each test consists of a well-formed zone file and a query that together causes execution to explore a particular RFC behavior.
   • Ferret takes approximately 2 hours for InvalidZoneFiles generation to generate 900 ill-formed zone files, 100 violating each of the validity conditions.
   CLICK to show the Results folder tree after test generation

    Results
    ├── ValidZoneFileTests
    │    └── ZenTests
    │        ├── 0.json
    │        ├── 1.json
    │        ├── ...
    │        └── 12673.json
    └── InvalidZoneFileTests
        ├── FalseCond_1
        │   └── ZenZoneFiles
        │       ├── 0.json
        │       ├── 1.json
        │       ├── ...
        │       └── 99.json
        ├── FalseCond_2
        │   └── ZenZoneFiles
        │       ├── 0.json
        │       ├── 1.json
        │       ├── ...
        │       └── 99.json
        ├── ...
        └── FalseCond_9
            └── ZenZoneFiles
                ├── 0.json
                ├── 1.json
                ├── ...
                └── 99.json

After the tests are generated, go to the Differential testing module.