symex-intro

Material for an introductory presentation for symbolic execution.

git clone https://git.8pit.net/symex-intro.git

  1/*
  2 * SPDX-FileCopyrightText: 2014 HAW Hamburg
  3 * SPDX-FileCopyrightText: 2014 Martin Landsmann <Martin.Landsmann@HAW-Hamburg.de>
  4 * SPDX-FileCopyrightText: 2020 Otto-von-Guericke-Universität Magdeburg
  5 * SPDX-License-Identifier: LGPL-2.1-only
  6 */
  7
  8/**
  9 * @ingroup sys_base64
 10 * @{
 11 * @file
 12 * @brief   Functions to encode and decode base64
 13 *
 14 * @author  Martin Landsmann <Martin.Landsmann@HAW-Hamburg.de>
 15 * @author  Marian Buschsieweke <marian.buschsieweke@ovgu.de>
 16 * @}
 17 *
 18 */
 19
 20#include <assert.h>
 21#include <string.h>
 22#include <stdbool.h>
 23#include <stdint.h>
 24#include <klee/klee.h>
 25
 26#include "base64.h"
 27
 28// Uncomment to enable state merging, causing a speed up by merging paths.
 29//#define KLEE_STATE_MERGING 1
 30
 31// Whether to enable URL-safe base64.
 32#define BASE64URLSAFE 0
 33
 34#define BASE64_CAPITAL_UPPER_BOUND     (25)     /**< base64 'Z'           */
 35#define BASE64_SMALL_UPPER_BOUND       (51)     /**< base64 'z'           */
 36#define BASE64_NUMBER_UPPER_BOUND      (61)     /**< base64 '9'           */
 37#define BASE64_PLUS                    (62)     /**< base64 '+'           */
 38#define BASE64_MINUS                   (62)     /**< base64 '-'           */
 39#define BASE64_SLASH                   (63)     /**< base64 '/'           */
 40#define BASE64_UNDERLINE               (63)     /**< base64 '_'           */
 41#define BASE64_EQUALS                  (0xFE)   /**< no base64 symbol '=' */
 42#define BASE64_NOT_DEFINED             (0xFF)   /**< no base64 symbol     */
 43
 44/*
 45 * returns the corresponding ascii symbol value for the given base64 code
 46 */
 47static char __getsymbol(uint8_t code, bool urlsafe)
 48{
 49    if (!BASE64URLSAFE) {
 50        urlsafe = false;
 51    }
 52
 53    if (urlsafe && code == BASE64_UNDERLINE) {
 54        return '_';
 55    }
 56
 57    if (urlsafe && code == BASE64_MINUS) {
 58        return '-';
 59    }
 60
 61    if (!urlsafe && code == BASE64_SLASH) {
 62        return '/';
 63    }
 64
 65    if (!urlsafe && code == BASE64_PLUS) {
 66        return '+';
 67    }
 68
 69    if (code <= BASE64_CAPITAL_UPPER_BOUND) {
 70        return (code + 'A');
 71    }
 72
 73    if (code <= BASE64_SMALL_UPPER_BOUND) {
 74        return (code + ('z' - BASE64_SMALL_UPPER_BOUND));
 75    }
 76
 77    if (code <= BASE64_NUMBER_UPPER_BOUND) {
 78        return (code + ('9' - BASE64_NUMBER_UPPER_BOUND));
 79    }
 80
 81    return (char)BASE64_NOT_DEFINED;
 82}
 83
 84static char getsymbol(uint8_t code, bool urlsafe)
 85{
 86#ifdef KLEE_STATE_MERGING
 87    klee_open_merge();
 88#endif
 89    char ret = __getsymbol(code, urlsafe);
 90#ifdef KLEE_STATE_MERGING
 91    klee_close_merge();
 92#endif
 93    return ret;
 94}
 95
 96static void encode_three_bytes(uint8_t *dest,
 97                               uint8_t b1, uint8_t b2, uint8_t b3,
 98                               bool urlsafe)
 99{
100    dest[0] = getsymbol(b1 >> 2, urlsafe);
101    dest[1] = getsymbol(((b1 & 0x03) << 4) | (b2 >> 4), urlsafe);
102    dest[2] = getsymbol(((b2 & 0x0f) << 2) | (b3 >> 6), urlsafe);
103    dest[3] = getsymbol(b3 & 0x3f, urlsafe);
104}
105
106static int base64_encode_base(const void *data_in, size_t data_in_size,
107                              void *base64_out, size_t *base64_out_size,
108                              bool urlsafe)
109{
110    const uint8_t padding = urlsafe ? 0 : '=';
111    const uint8_t *in = data_in;
112    uint8_t *out = base64_out;
113
114    if (in == NULL) {
115        return BASE64_ERROR_DATA_IN;
116    }
117
118    if (data_in_size == 0) {
119        *base64_out_size = 0;
120        return BASE64_SUCCESS;
121    }
122
123    if (!base64_can_estimate_encode_size(data_in_size)) {
124        return BASE64_ERROR_OVERFLOW;
125    }
126
127    size_t required_size = base64_estimate_encode_size(data_in_size);
128
129    if (*base64_out_size < required_size) {
130        *base64_out_size = required_size;
131        return BASE64_ERROR_BUFFER_OUT_SIZE;
132    }
133
134    if (out == NULL) {
135        return BASE64_ERROR_BUFFER_OUT;
136    }
137
138    *base64_out_size = required_size;
139
140    const uint8_t *end = in + data_in_size;
141
142    while (in < end - 2) {
143        encode_three_bytes(out, in[0], in[1], in[2], urlsafe);
144        out += 4;
145        in += 3;
146    }
147
148    if (in == end) {
149        /* data_in_size is multiple of 3, we're done */
150        return BASE64_SUCCESS;
151    }
152
153    if (in + 1 == end) {
154        /* One byte still left to decode, set other two input bytes to zero */
155        encode_three_bytes(out, in[0], 0, 0, urlsafe);
156        /* Replace last two bytes with "=" to signal corresponding input bytes
157         * didn't exist */
158        out[2] = out[3] = padding;
159
160        /* padding is not required for urlsafe application */
161        if (urlsafe) {
162            *base64_out_size -= 2;
163        }
164        return BASE64_SUCCESS;
165    }
166
167    /* Final case: 2 bytes remain for encoding, use zero as third input */
168    encode_three_bytes(out, in[0], in[1], 0, urlsafe);
169    /* Replace last output with "=" to signal corresponding input byte didn't exit */
170    out[3] = padding;
171
172    /* padding is not required for urlsafe application */
173    if (urlsafe) {
174        *base64_out_size -= 1;
175    }
176
177    return BASE64_SUCCESS;
178}
179
180int base64_encode(const void *data_in, size_t data_in_size,
181                  void *base64_out, size_t *base64_out_size)
182{
183    return base64_encode_base(data_in, data_in_size, base64_out, base64_out_size, false);
184}
185
186#if BASE64URLSAFE
187int base64url_encode(const void *data_in, size_t data_in_size,
188                     void *base64_out, size_t *base64_out_size)
189{
190    return base64_encode_base(data_in, data_in_size, base64_out, base64_out_size, true);
191}
192#endif
193
194/*
195 *  returns the corresponding base64 code for the given ascii symbol
196 */
197static uint8_t __getcode(char symbol)
198{
199    if (symbol == '/') {
200        return BASE64_SLASH;
201    }
202
203    if (symbol == '_') {
204        return BASE64_UNDERLINE;
205    }
206
207    if (symbol == '+') {
208        return BASE64_PLUS;
209    }
210
211    if (symbol == '-') {
212        return BASE64_MINUS;
213    }
214
215    if (symbol == '=') {
216        /* indicates a padded base64 end */
217        return BASE64_EQUALS;
218    }
219
220    if (symbol < '0') {
221        /* indicates that the given symbol is not base64 and should be ignored */
222        return BASE64_NOT_DEFINED;
223    }
224
225    if (symbol <= '9' && symbol >= '0') {
226        return (symbol + (BASE64_NUMBER_UPPER_BOUND - '9'));
227    }
228
229    if (symbol <= 'Z' && symbol >= 'A') {
230        return (symbol - 'A');
231    }
232
233    if (symbol <= 'z' && symbol >= 'a') {
234        return (symbol + (BASE64_SMALL_UPPER_BOUND - 'z'));
235    }
236
237    /* indicates that the given symbol is not base64 and should be ignored */
238    return BASE64_NOT_DEFINED;
239}
240
241static uint8_t getcode(char symbol)
242{
243#ifdef KLEE_STATE_MERGING
244    klee_open_merge();
245#endif
246    uint8_t ret = __getcode(symbol);
247#ifdef KLEE_STATE_MERGING
248    klee_close_merge();
249#endif
250    return ret;
251}
252
253static void decode_four_codes(uint8_t *out, const uint8_t *src)
254{
255    out[0] = (src[0] << 2) | (src[1] >> 4);
256    out[1] = (src[1] << 4) | (src[2] >> 2);
257    out[2] = (src[2] << 6) | src[3];
258}
259
260int base64_decode(const void *base64_in, size_t base64_in_size,
261                  void *data_out, size_t *data_out_size)
262{
263    const uint8_t *in = base64_in;
264    uint8_t *out = data_out;
265
266    if (in == NULL) {
267        return BASE64_ERROR_DATA_IN;
268    }
269
270    if (base64_in_size == 0) {
271        *data_out_size = 0;
272        return BASE64_SUCCESS;
273    }
274
275    size_t required_size = base64_estimate_decode_size(base64_in_size);
276
277    if (*data_out_size < required_size) {
278        *data_out_size = required_size;
279        return BASE64_ERROR_BUFFER_OUT_SIZE;
280    }
281
282    if (data_out == NULL) {
283        return BASE64_ERROR_BUFFER_OUT;
284    }
285
286    const uint8_t *end = in + base64_in_size;
287    uint8_t decode_buf[4];
288
289    while (1) {
290        size_t decode_buf_fill = 0;
291        /* Try to load 4 codes into the decode buffer, skipping invalid symbols
292         * (such as inserted newlines commonly used to improve readability) */
293        do {
294            /* Reached end of input before 4 codes were loaded, handle each
295             * possible decode buffer fill level individually: */
296            if (in == end) {
297                switch (decode_buf_fill) {
298                    case 0:
299                        /* no data in decode buffer -->nothing to do */
300                        break;
301                    case 1:
302                        /* an input size of 4 * n + 1 cannot happen, (even when
303                         * dropping the "=" chars) */
304                        return BASE64_ERROR_DATA_IN_SIZE;
305                    case 2:
306                        /* Got two base64 chars, or one byte of output data.
307                         * The just fill with zero codes and ignore the two
308                         * additionally decoded bytes */
309                        decode_buf[2] = decode_buf[3] = 0;
310                        decode_four_codes(out, decode_buf);
311                        out += 1;
312                        break;
313                    case 3:
314                        /* Got three base64 chars or 2 bytes of output data.
315                         * Again, just fill with zero bytes and ignore the
316                         * additionally decoded byte */
317                        decode_buf[3] = 0;
318                        decode_four_codes(out, decode_buf);
319                        out += 2;
320                        break;
321                }
322                *data_out_size = (uintptr_t)out - (uintptr_t)data_out;
323                return BASE64_SUCCESS;
324            }
325            switch (decode_buf[decode_buf_fill] = getcode(*in++)) {
326                case BASE64_NOT_DEFINED:
327                case BASE64_EQUALS:
328                    continue;
329            }
330            decode_buf_fill++;
331        }
332        while (decode_buf_fill < 4);
333
334        decode_four_codes(out, decode_buf);
335        out += 3;
336    }
337}
338
339////////////////////////////////////////////////////////////////////////
340
341int main(void) {
342    char input[INPUT_SIZE];
343    klee_make_symbolic(input, sizeof(input), "input");
344
345    char in[128];
346    size_t in_size = sizeof(in);
347    base64_encode(input, sizeof(input), in, &in_size);
348
349    char out[128];
350    size_t out_size = sizeof(out);
351    base64_decode(in, in_size, out, &out_size);
352
353    assert(out_size == INPUT_SIZE);
354    assert(memcmp(input, out, out_size) == 0);
355
356    return 0;
357}