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        // XXX: Uncomment to introduce an exemplary bug.
 71        //return (code + 'B');
 72        return (code + 'A');
 73    }
 74
 75    if (code <= BASE64_SMALL_UPPER_BOUND) {
 76        return (code + ('z' - BASE64_SMALL_UPPER_BOUND));
 77    }
 78
 79    if (code <= BASE64_NUMBER_UPPER_BOUND) {
 80        return (code + ('9' - BASE64_NUMBER_UPPER_BOUND));
 81    }
 82
 83    return (char)BASE64_NOT_DEFINED;
 84}
 85
 86static char getsymbol(uint8_t code, bool urlsafe)
 87{
 88#ifdef KLEE_STATE_MERGING
 89    klee_open_merge();
 90#endif
 91    char ret = __getsymbol(code, urlsafe);
 92#ifdef KLEE_STATE_MERGING
 93    klee_close_merge();
 94#endif
 95    return ret;
 96}
 97
 98static void encode_three_bytes(uint8_t *dest,
 99                               uint8_t b1, uint8_t b2, uint8_t b3,
100                               bool urlsafe)
101{
102    dest[0] = getsymbol(b1 >> 2, urlsafe);
103    dest[1] = getsymbol(((b1 & 0x03) << 4) | (b2 >> 4), urlsafe);
104    dest[2] = getsymbol(((b2 & 0x0f) << 2) | (b3 >> 6), urlsafe);
105    dest[3] = getsymbol(b3 & 0x3f, urlsafe);
106}
107
108static int base64_encode_base(const void *data_in, size_t data_in_size,
109                              void *base64_out, size_t *base64_out_size,
110                              bool urlsafe)
111{
112    const uint8_t padding = urlsafe ? 0 : '=';
113    const uint8_t *in = data_in;
114    uint8_t *out = base64_out;
115
116    if (in == NULL) {
117        return BASE64_ERROR_DATA_IN;
118    }
119
120    if (data_in_size == 0) {
121        *base64_out_size = 0;
122        return BASE64_SUCCESS;
123    }
124
125    if (!base64_can_estimate_encode_size(data_in_size)) {
126        return BASE64_ERROR_OVERFLOW;
127    }
128
129    size_t required_size = base64_estimate_encode_size(data_in_size);
130
131    if (*base64_out_size < required_size) {
132        *base64_out_size = required_size;
133        return BASE64_ERROR_BUFFER_OUT_SIZE;
134    }
135
136    if (out == NULL) {
137        return BASE64_ERROR_BUFFER_OUT;
138    }
139
140    *base64_out_size = required_size;
141
142    const uint8_t *end = in + data_in_size;
143
144    while (in < end - 2) {
145        encode_three_bytes(out, in[0], in[1], in[2], urlsafe);
146        out += 4;
147        in += 3;
148    }
149
150    if (in == end) {
151        /* data_in_size is multiple of 3, we're done */
152        return BASE64_SUCCESS;
153    }
154
155    if (in + 1 == end) {
156        /* One byte still left to decode, set other two input bytes to zero */
157        encode_three_bytes(out, in[0], 0, 0, urlsafe);
158        /* Replace last two bytes with "=" to signal corresponding input bytes
159         * didn't exist */
160        out[2] = out[3] = padding;
161
162        /* padding is not required for urlsafe application */
163        if (urlsafe) {
164            *base64_out_size -= 2;
165        }
166        return BASE64_SUCCESS;
167    }
168
169    /* Final case: 2 bytes remain for encoding, use zero as third input */
170    encode_three_bytes(out, in[0], in[1], 0, urlsafe);
171    /* Replace last output with "=" to signal corresponding input byte didn't exit */
172    out[3] = padding;
173
174    /* padding is not required for urlsafe application */
175    if (urlsafe) {
176        *base64_out_size -= 1;
177    }
178
179    return BASE64_SUCCESS;
180}
181
182int base64_encode(const void *data_in, size_t data_in_size,
183                  void *base64_out, size_t *base64_out_size)
184{
185    return base64_encode_base(data_in, data_in_size, base64_out, base64_out_size, false);
186}
187
188#if BASE64URLSAFE
189int base64url_encode(const void *data_in, size_t data_in_size,
190                     void *base64_out, size_t *base64_out_size)
191{
192    return base64_encode_base(data_in, data_in_size, base64_out, base64_out_size, true);
193}
194#endif
195
196/*
197 *  returns the corresponding base64 code for the given ascii symbol
198 */
199static uint8_t __getcode(char symbol)
200{
201    if (symbol == '/') {
202        return BASE64_SLASH;
203    }
204
205    if (symbol == '_') {
206        return BASE64_UNDERLINE;
207    }
208
209    if (symbol == '+') {
210        return BASE64_PLUS;
211    }
212
213    if (symbol == '-') {
214        return BASE64_MINUS;
215    }
216
217    if (symbol == '=') {
218        /* indicates a padded base64 end */
219        return BASE64_EQUALS;
220    }
221
222    if (symbol < '0') {
223        /* indicates that the given symbol is not base64 and should be ignored */
224        return BASE64_NOT_DEFINED;
225    }
226
227    if (symbol <= '9' && symbol >= '0') {
228        return (symbol + (BASE64_NUMBER_UPPER_BOUND - '9'));
229    }
230
231    if (symbol <= 'Z' && symbol >= 'A') {
232        return (symbol - 'A');
233    }
234
235    if (symbol <= 'z' && symbol >= 'a') {
236        return (symbol + (BASE64_SMALL_UPPER_BOUND - 'z'));
237    }
238
239    /* indicates that the given symbol is not base64 and should be ignored */
240    return BASE64_NOT_DEFINED;
241}
242
243static uint8_t getcode(char symbol)
244{
245#ifdef KLEE_STATE_MERGING
246    klee_open_merge();
247#endif
248    uint8_t ret = __getcode(symbol);
249#ifdef KLEE_STATE_MERGING
250    klee_close_merge();
251#endif
252    return ret;
253}
254
255static void decode_four_codes(uint8_t *out, const uint8_t *src)
256{
257    out[0] = (src[0] << 2) | (src[1] >> 4);
258    out[1] = (src[1] << 4) | (src[2] >> 2);
259    out[2] = (src[2] << 6) | src[3];
260}
261
262int base64_decode(const void *base64_in, size_t base64_in_size,
263                  void *data_out, size_t *data_out_size)
264{
265    const uint8_t *in = base64_in;
266    uint8_t *out = data_out;
267
268    if (in == NULL) {
269        return BASE64_ERROR_DATA_IN;
270    }
271
272    if (base64_in_size == 0) {
273        *data_out_size = 0;
274        return BASE64_SUCCESS;
275    }
276
277    size_t required_size = base64_estimate_decode_size(base64_in_size);
278
279    if (*data_out_size < required_size) {
280        *data_out_size = required_size;
281        return BASE64_ERROR_BUFFER_OUT_SIZE;
282    }
283
284    if (data_out == NULL) {
285        return BASE64_ERROR_BUFFER_OUT;
286    }
287
288    const uint8_t *end = in + base64_in_size;
289    uint8_t decode_buf[4];
290
291    while (1) {
292        size_t decode_buf_fill = 0;
293        /* Try to load 4 codes into the decode buffer, skipping invalid symbols
294         * (such as inserted newlines commonly used to improve readability) */
295        do {
296            /* Reached end of input before 4 codes were loaded, handle each
297             * possible decode buffer fill level individually: */
298            if (in == end) {
299                switch (decode_buf_fill) {
300                    case 0:
301                        /* no data in decode buffer -->nothing to do */
302                        break;
303                    case 1:
304                        /* an input size of 4 * n + 1 cannot happen, (even when
305                         * dropping the "=" chars) */
306                        return BASE64_ERROR_DATA_IN_SIZE;
307                    case 2:
308                        /* Got two base64 chars, or one byte of output data.
309                         * The just fill with zero codes and ignore the two
310                         * additionally decoded bytes */
311                        decode_buf[2] = decode_buf[3] = 0;
312                        decode_four_codes(out, decode_buf);
313                        out += 1;
314                        break;
315                    case 3:
316                        /* Got three base64 chars or 2 bytes of output data.
317                         * Again, just fill with zero bytes and ignore the
318                         * additionally decoded byte */
319                        decode_buf[3] = 0;
320                        decode_four_codes(out, decode_buf);
321                        out += 2;
322                        break;
323                }
324                *data_out_size = (uintptr_t)out - (uintptr_t)data_out;
325                return BASE64_SUCCESS;
326            }
327            switch (decode_buf[decode_buf_fill] = getcode(*in++)) {
328                case BASE64_NOT_DEFINED:
329                case BASE64_EQUALS:
330                    continue;
331            }
332            decode_buf_fill++;
333        }
334        while (decode_buf_fill < 4);
335
336        decode_four_codes(out, decode_buf);
337        out += 3;
338    }
339}
340
341////////////////////////////////////////////////////////////////////////
342
343int main(void) {
344    char input[INPUT_SIZE];
345    klee_make_symbolic(input, sizeof(input), "input");
346
347    char in[128];
348    size_t in_size = sizeof(in);
349    base64_encode(input, sizeof(input), in, &in_size);
350
351    char out[128];
352    size_t out_size = sizeof(out);
353    base64_decode(in, in_size, out, &out_size);
354
355    assert(out_size == INPUT_SIZE);
356    assert(memcmp(input, out, out_size) == 0);
357
358    return 0;
359}