summaryrefslogtreecommitdiffstats
path: root/pickles/luks.pk
blob: 460fa3b11cd2de661bedff103ba65ffcedce88a8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
/* Linux Unified Key Setup (LUKS) module, by apache2

  See the specifications for LUKS1 and LUKS2:
https://gitlab.com/cryptsetup/cryptsetup/-/wikis/LUKS-standard/on-disk-format.pdf
https://github.com/mbroz/cryptsetup/blob/master/docs/on-disk-format-luks2.pdf

  And the header files:
https://gitlab.com/cryptsetup/cryptsetup/-/blob/master/lib/luks1/luks.h
https://gitlab.com/cryptsetup/cryptsetup/-/blob/master/lib/luks2/luks2.h

  How to test:
truncate -s 1M test.luks
cryptsetup luksFormat test.luks
poke -l luks.pk -c '.set pretty-print yes' -c '.set omode tree' -c '(LUKS_header @ open("./test.luks") : 0#B)'

  This is probably not so useful for LUKS2 since most of the data is kept in
  the JSON data structure.
*/

set_endian (ENDIAN_BIG); // all fields are big-endian, see LUKS2:2.1

type LUKS_key_slot = struct
  {
    union {
      uint<32> DISABLED : DISABLED in [0, 0xDEAD];
      uint<32> ENABLED : ENABLED in [0xCAFE, 0xAC71F3];
    } active;
    uint<32> iterations;
    byte[32] salt;
    uint<32> key_material_offset;
    uint<32> stripes;
  };
assert(sizeof(LUKS_key_slot) == 48#B);

var LUKS_MAGIC_1ST = [ 'L','U','K','S', 0xbaUB, 0xbeUB ],
    LUKS_MAGIC_2ND = [ 'S','K','U','L', 0xbaUB, 0xbeUB ];

type LUKS_phdr_v1 = struct
  {
    char[6] magic == LUKS_MAGIC_1ST;
    uint<16> version == 1;
    char[32] cipher_name;
    char[32] cipher_mode;
    char[32] hash_spec;
    offset<uint<32>,512B> payload_offset;
    uint<32> key_bytes; // masterKey
    byte[20] mk_digest;
    byte[32] mk_digest_salt;
    uint<32> mk_digest_iter;
    char[40] uuid;
    LUKS_key_slot[8] key_slots;
  }; assert (sizeof(LUKS_phdr_v1) == 592#B);

/*
 * To deal with padding below we pin e.g. csum_alg, which comes after a
 * variable-length "string label;", to
 * OFFSET (first byte after the previous field)
 * - label'size (actual variable size of label, including trailing \0)
 * + maximum size of label (48#B in this case).
 * Note that in practice we could also have used a char[48] label;
 * to express this, but this way we get an implicit constraint that it must
 * contain at least one zerobyte, and the pretty-printer will look nicer:
 */

type LUKS_phdr_v2 = struct
  {
  /* MAGIC_1st for the primary header and MAGIC_2nd for the secondary header */
    char[6] magic;
    uint<16> version == 2;
    offset<uint<64>,B> hdr_size : hdr_size >= 4096#B; // including json area
    uint<64> seqid; // increased on update to detect broken updates
    string label : label'size <= 48#B;
    string csum_alg : csum_alg'size <= 32#B
        @ OFFSET - label'size + 48#B; // checksum algorith, eg "sha256"
    byte[64] salt @ OFFSET - csum_alg'size + 32#B;
    string uuid : uuid'size <= 40#B;
    string subsystem : subsystem'size <= 48#B @ OFFSET - uuid'size + 40#B;
    offset<uint<64>,B> hdr_offset @ OFFSET - subsystem'size+48#B;
    byte[64] csum @ OFFSET + 184#B; /* hash of |LUKS2_bin|LUKS2_JSON_area| */
    byte[0] @ OFFSET + 3584#B;
  };

type LUKS_header = struct
  {
    union {
        LUKS_phdr_v1 v1;
        struct {
            LUKS_phdr_v2 primary : (primary.magic == LUKS_MAGIC_1ST
                                 && primary.hdr_offset == 0#B
            /* the constraint below comes from table 1 in the luks2 on-disk spec: */
                                 && primary.hdr_size in [
                                 0x004000#B,
                                 0x008000#B,
                                 0x010000#B,
                                 0x020000#B,
                                 0x040000#B,
                                 0x080000#B,
                                 0x100000#B,
                                 0x200000#B,
                                 0x400000#B]);
           string primary_json : ( primary_json'size <= primary.hdr_size-4096#B);
           LUKS_phdr_v2 secondary : (secondary.magic == LUKS_MAGIC_2ND
                                  && secondary.hdr_offset==primary.hdr_size
                                  && OFFSET <= primary.hdr_size)
               @ primary.hdr_size ;
           string secondary_json : secondary_json'size <= secondary.hdr_size - 4096#B;
    } v2;
    } phdr;
  /* after this, keyslots and anti-forensic splitting material. */
  };
Generated by cgit on ageinghacker.net.
I am Luca Saiu. If you have reason to request commit access to one of these repositories please contact me. You may also send me patches by email.