Example

Consider a typical 128-bit block cipher, which produces a a 128-bit ciphertext c by encrypting a 128-bit plaintext m using a 128-bit cipher key k. This example demonstrates how a FIAT-supported target implementation reflecting such a block cipher, or at least a trivial proxy for one, could be developed and used. To do so, we use the native build context and board type: this allows the target implementation to be built and executed on the development platform itself with no real dependencies (e.g., with an installation of GCC already available), and thus offers a way to prototype and debug both target and client implementations.

Step 3: develop target implementation

  1. We configure the target implementation by editing

    ${FIAT_PATH_REPO}/src/fiat/target/kernel/imp/kernel_imp.conf

    In particular, we replace the existing register declarations with

    DECLARE_GPR(c, 16, {}, .wr = false, .rd =  true, .length = KERNEL_REG_LENGTH_FIX)
DECLARE_GPR(k, 16, {}, .wr =  true, .rd = false, .length = KERNEL_REG_LENGTH_FIX)
DECLARE_GPR(m, 16, {}, .wr =  true, .rd = false, .length = KERNEL_REG_LENGTH_FIX)

    Doing so means

    • c is a fixed-length, 16-byte RO (or output only) GPR with address 0x00 = 0,

    • k is a fixed-length, 16-byte WO (or input only) GPR with address 0x01 = 1, and

    • m is a fixed-length, 16-byte WO (or input only) GPR with address 0x02 = 2.

  2. We complete the target implementation by editing

    ${FIAT_PATH_REPO}/src/fiat/target/kernel/imp/kernel_imp.c

    In particular, we replace the kernel function with

    ret_t kernel( int op, kernel_reg_t* spr, kernel_reg_t* gpr ) {
  byte* c = gpr[ 0 ].data;
  byte* k = gpr[ 1 ].data;
  byte* m = gpr[ 2 ].data;

  for( int i = 0; i < 16; i++ ) {
    c[ i ] = k[ i ] ^ m[ i ];
  }

  return EXIT_SUCCESS;
}

    Doing so means c will be computed as k ^ m (i.e., XOR’ing k and m together).

Step 4: build target implementation

  • Either execute

    FIAT_CONTEXT="native" FIAT_DRIVER="binary" FIAT_BOARD="native" make target/clean target/build

    to use the binary driver, or

    FIAT_CONTEXT="native" FIAT_DRIVER="text"   FIAT_BOARD="native" make target/clean target/build

    to use the text driver.

Step 5: use target implementation

To drive interaction with the target implementation, we use an example client implementation located in

${FIAT_PATH_REPO}/src/fiat/client/script/example.py

whose core functionality is captured by the following fragment:

17if ( __name__ == '__main__' ) :
18  client = libfiat.open( sys.argv ) ; random.seed( 0 )
19
20  ( ack,   ) = client.reset()
21
22  for index in [ GPR_C, GPR_K, GPR_M ] :
23    ( ack, nameof ) = client.nameof( index )
24    print( 'nameof( 0x{0:02X} ) = {1:s}'.format( index, nameof ) )  
25
26  for index in [ GPR_C, GPR_K, GPR_M ] :
27    ( ack, sizeof ) = client.sizeof( index )
28    print( 'sizeof( 0x{0:02X} ) = {1:d}'.format( index, sizeof ) )
29
30  for index in [ GPR_C, GPR_K, GPR_M ] :
31    ( ack, typeof ) = client.typeof( index )
32    print( 'typeof( 0x{0:02X} ) = 0x{1:02X} => wr={2:d}, rd={3:d}, length={4:d}'.format( index, typeof, typeof.wr(), typeof.rd(), typeof.length() ) )
33
34  k = random.randbytes( 16 )
35  m = random.randbytes( 16 )
36
37  ( ack,   ) = client.wr( GPR_K, bytes( k ) )
38  ( ack,   ) = client.wr( GPR_M, bytes( m ) )
39
40  ( ack,   ) = client.kernel()
41
42  ( ack, c ) = client.rd( GPR_C             )
43
44  for i in range( 16 ) :
45    print( 'i = {0:2d} : c[i] = 0x{1:02X}, k[i] ^ m[i] = 0x{2:02X}'.format( i, c[ i ], k[ i ] ^ m[ i ] ) )
46
47  client.close()

Note that each line which issues a request does not, but ideally would check the associated acknowledgement: execution simply continues under the assumption that each acknowledgement indicates success. A line-by-line overview reads as follows:

  • line 18 opens the client (or connection),

  • line 20 issues a reset request,

  • lines 22 to 24 issue a series of nameof requests to query the identifier of c, k, and m registers,

  • lines 26 to 28 issue a series of sizeof requests to query the allocated size of c, k, and m registers,

  • lines 30 to 32 issue a series of typeof requests to query the type of c, k, and m registers (including, e.g., the read- and write-access),

  • lines 34 and 35 generate random, 16-byte values for k and m,

  • lines 37 and 38 issue a series of wr requests to write (i.e., transfer from client to target) k and m,

  • line 40 issues a kernel request to invoke the kernel function which computes c from k and m,

  • line 42 issues a rd request to read (i.e., transfer from client to target) c,

  • lines 44 and 45 print each byte of c and k ^ m to check whether the value read matches that expected,

  • line 47 closes the client (or connection).

Now we can execute the target and client, and interaction between them:

  • In terminal 1, execute

    ncat --verbose --listen --source-port 1234 --hex-dump ${FIAT_PATH_REPO}/build/target/native/target.ncat --exec ${FIAT_PATH_REPO}/build/target/native/target.elf

    Doing so uses ncat to execute the target implementation, and connect the associated stdin and stdout standard streams to a (local) network socket we can connect to. Notice that use of --hex-dump means that all communicated data will be captured in the file ${FIAT_PATH_REPO}/build/target/native/target.ncat

  • In terminal 2, install libfiat

    pip3 install libfiat

    then either execute

    python3 ${FIAT_PATH_REPO}/src/fiat/client/script/example.py --libfiat-device='socket' --libfiat-driver='binary' --libfiat-host='127.0.0.1' --libfiat-port='1234'

    to use the binary driver, or

    python3 ${FIAT_PATH_REPO}/src/fiat/client/script/example.py --libfiat-device='socket' --libfiat-driver='text'   --libfiat-host='127.0.0.1' --libfiat-port='1234'

    to use the text driver.

Using either driver, we expect an output similar to

 1nameof( 0x00 ) = c
 2nameof( 0x01 ) = k
 3nameof( 0x02 ) = m
 4sizeof( 0x00 ) = 16
 5sizeof( 0x01 ) = 16
 6sizeof( 0x02 ) = 16
 7typeof( 0x00 ) = 0x02 => wr=0, rd=1, length=0
 8typeof( 0x01 ) = 0x01 => wr=1, rd=0, length=0
 9typeof( 0x02 ) = 0x01 => wr=1, rd=0, length=0
10i =  0 : c[i] = 0x98, k[i] ^ m[i] = 0x98
11i =  1 : c[i] = 0x93, k[i] ^ m[i] = 0x93
12i =  2 : c[i] = 0x86, k[i] ^ m[i] = 0x86
13i =  3 : c[i] = 0xB3, k[i] ^ m[i] = 0xB3
14i =  4 : c[i] = 0x8A, k[i] ^ m[i] = 0x8A
15i =  5 : c[i] = 0x40, k[i] ^ m[i] = 0x40
16i =  6 : c[i] = 0xC2, k[i] ^ m[i] = 0xC2
17i =  7 : c[i] = 0x68, k[i] ^ m[i] = 0x68
18i =  8 : c[i] = 0x96, k[i] ^ m[i] = 0x96
19i =  9 : c[i] = 0x12, k[i] ^ m[i] = 0x12
20i = 10 : c[i] = 0x41, k[i] ^ m[i] = 0x41
21i = 11 : c[i] = 0x80, k[i] ^ m[i] = 0x80
22i = 12 : c[i] = 0x78, k[i] ^ m[i] = 0x78
23i = 13 : c[i] = 0xB2, k[i] ^ m[i] = 0xB2
24i = 14 : c[i] = 0xCF, k[i] ^ m[i] = 0xCF
25i = 15 : c[i] = 0x14, k[i] ^ m[i] = 0x14

noting that despite use of random.randbytes( 16 ) to generate k and m, they, and thus c, should match the above due to the fixed seed provided via random.seed( 0 ). Either way, the important feature is that each c[i] received from the target implementation matches the k[i] ^ m[i] we compute locally: this demonstrates it is operating as expected.

  • From use of the binary driver, ${FIAT_PATH_REPO}/build/target/native/target.ncat reads as follows:

     1[0000]   2A 58 8E                                            *X.
 2[0000]   2B D1 9F                                            +..
 3[0000]   22 00 83 10                                         "...
 4[0000]   2B 01 63 D8 62                                      +.c.b
 5[0000]   22 01 0A 01                                         "...
 6[0000]   2B 01 6B 90 EE                                      +.k..
 7[0000]   22 02 91 33                                         "..3
 8[0000]   2B 01 6D A6 8B                                      +.m..
 9[0000]   7C 00 64 59                                         |.dY
10[0000]   2B 10 1A D7                                         +...
11[0000]   7C 01 ED 48                                         |..H
12[0000]   2B 10 1A D7                                         +...
13[0000]   7C 02 76 7A                                         |.vz
14[0000]   2B 10 1A D7                                         +...
15[0000]   3F 00 6A 35                                         ?.j5
16[0000]   2B 02 89 E4                                         +...
17[0000]   3F 01 E3 24                                         ?..$
18[0000]   2B 01 12 D6                                         +...
19[0000]   3F 02 78 16                                         ?.x.
20[0000]   2B 01 12 D6                                         +...
21[0000]   3E 01 10 CD 07 2C D8 BE   6F 9F 62 AC 4C 09 C2 82   >....,.. o.b.L...
22[0010]   06 E7 E3 EB 60                                      ....`
23[0000]   2B D1 9F                                            +..
24[0000]   3E 02 10 55 94 AA 6B 34   2F 5D 0A 3A 5E 48 42 FA   >..U..k4 /].:^HB.
25[0010]   B4 28 F7 64 EC                                      .(.d.
26[0000]   2B D1 9F                                            +..
27[0000]   3D 00 01 58 68                                      =..Xh
28[0000]   2B D1 9F                                            +..
29[0000]   3C 00 02 1F                                         <...
30[0000]   2B 10 98 93 86 B3 8A 40   C2 68 96 12 41            +......@ .h..A
31[0000]   80 78 B2 CF 14 2E 9E                                .x.....

  • From use of the text driver, ${FIAT_PATH_REPO}/build/target/native/target.ncat reads as follows:

     1[0000]   2A 58 8E                                            *X.
 2[0000]   2B D1 9F                                            +..
 3[0000]   22 00 83 10                                         "...
 4[0000]   2B 01 63 D8 62                                      +.c.b
 5[0000]   22 01 0A 01                                         "...
 6[0000]   2B 01 6B 90 EE                                      +.k..
 7[0000]   22 02 91 33                                         "..3
 8[0000]   2B 01 6D A6 8B                                      +.m..
 9[0000]   7C 00 64 59                                         |.dY
10[0000]   2B 10 1A D7                                         +...
11[0000]   7C 01 ED 48                                         |..H
12[0000]   2B 10 1A D7                                         +...
13[0000]   7C 02 76 7A                                         |.vz
14[0000]   2B 10 1A D7                                         +...
15[0000]   3F 00 6A 35                                         ?.j5
16[0000]   2B 02 89 E4                                         +...
17[0000]   3F 01 E3 24                                         ?..$
18[0000]   2B 01 12 D6                                         +...
19[0000]   3F 02 78 16                                         ?.x.
20[0000]   2B 01 12 D6                                         +...
21[0000]   3E 01 10 CD 07 2C D8 BE   6F 9F 62 AC 4C 09 C2 82   >....,.. o.b.L...
22[0010]   06 E7 E3 EB 60                                      ....`
23[0000]   2B D1 9F                                            +..
24[0000]   3E 02 10 55 94 AA 6B 34   2F 5D 0A 3A 5E 48 42 FA   >..U..k4 /].:^HB.
25[0010]   B4 28 F7 64 EC                                      .(.d.
26[0000]   2B D1 9F                                            +..
27[0000]   3D 00 01 58 68                                      =..Xh
28[0000]   2B D1 9F                                            +..
29[0000]   3C 00 02 1F                                         <...
30[0000]   2B 10 98 93 86 B3 8A 40   C2 68 96 12 41            +......@ .h..A
31[0000]   80 78 B2 CF 14 2E 9E                                .x.....