print · source · login   

The Mapper

As described in the benchmark description, only the ReadFile message has a parameter called file, which can take on integer values in the range from 256 up to (and including) 511. Actually, each of these numbers has to be considered separately in the inference process, which would require a lot of time and memory space. By taking a closer look at the informal specification of the passport, we discovered that different files should be treated in the same way by the SUT. As one can see in Figure 1, files 257 and 258 should be readable after a BAC, 259 after a BAC followed by an EAC and the rest of the files should never be readable. Using this a priori knowledge about the passport, we can divide the values into three disjoint equivalence classes, which are:

  • ValidAfterBAC refers to the les that can be read after a BAC, i.e. 257 and 258.
  • ValidAfterEAC refers to the les that only can be read after a BAC followed by an EAC, i.e. 259.
  • NotValid refers to the les that can never be read, i.e. all les except for 257, 258 and 259.

In the abstraction mapping an abstract value is translated to a concrete one by randomly choosing an element within the corresponding equivalence class. If the numbers are partitioned incorrectly, then there are two values in the same class that produce a different response, which will give an error message.

The Learned Model

Learned model of the biometric passport
Fig. 2: Learned model of the biometric passport