En este práctico vamos a descubrir unas funcionalidades de CBMC, una herramienta que puede ser usada para ejecutar una verificación acotada (bounded model checking) directamente sobre código C. Permite al usuario averiguar directamente ciertas aserciones, pero también puede averiguar si hay problemas potenciales con punteros y límites de índices de arreglos. También puede verificar ciertas partes de un código sin borrar otras partes. Por supuesto, como lleva a cabo un model checking acotado, tiene problemas cuando se encuentra con bucles infinitos, pero también es capaz de limitar la cantidad de veces que se repite un bucle, e incluso detectar si se pierde algun comportamiento haciéndolo (es decir, si el bucle infinito no era realmente infinito).

Encontrarás más detalles sobre CBMC en el manual, la página del proyecto, o la documentación de la API.

En este práctico de laboratorio, se tratará de ver un pantallazo de las funcionalidades básicas de CBMC con el objetivo de entender su comportamiento y salida. Si lo terminás, te recomiendo de verificar tu propio código C.

Ejercicio 1: aserciones

  1. Bajá este código, y abrilo. ¿Qué intenta verificar? ¿Creés que es cierto?
  2. Ejecutá cbmc file.c. ¿Qué ocurre?
  3. cbmc file.c --show-claims te muestra todos los claims (afirmaciones, aserciones) que CBMC intenta verificar (con nombre y detalles).
  4. cbmc file.c --claim main.assertion.1 te permite averiguar una sola aserción.
  5. CBMC convierte el programa y sus aserciones en fórmulas de lógica proposicional, y se la da a un SAT solver. Podés ver qué es esa fórmula con la opción --show-vcc. Si agregás la opción --slice-formula, solo te mostrará las restricciones que son relevantes para cada aserción (tal vez es más fácil de leer).

Ejercicio 2: assumptions

  1. Bajá este código, abrilo, y verificalo con CBMC (usá las opciones que vimos más arriba). ¿Qué hace la función __CPROVER_assume? ¿Qué pasa si la sacás?
  2. Bajá este otro código. ¿La verificación es exitosa? ¿Porqué?

Ejercicio 3: límites de arreglos

  1. Bajá este código. ¿Hay algún problema?
  2. Ejecutá cbmc tableau.c. ¿Qué pasa?
  3. CBMC puede averiguar si el programa intenta salir de los límites de un arreglo. Para eso, debés usar la opción --bounds-check. ¿Qué pasa si lo hacés?
  4. Utilizá esta opción en conjunto con las opciones anteriores para explorar qué hace CBMC.

Ejercicio 4: punteros

  1. Bajá este código. ¿Ves algún problema?
  2. Ejecutá CBMC sobre él (sin, y luego con --bounds-check). ¿Qué ocurre?
  3. CBMC es también capaz de darse cuenta si algo raro ocurre con los punteros (acceso a memoria no autorizada, desreferenciación ilegal, etc.). Eso se hace con la opción --pointer-check. Utilizala.
  4. Tratá de entender qué está pasando (sin las opciones anteriores).

Ejercicio 5: bucles y subprogramas

  1. Bajá este código. ¿Qué debería pasar?
  2. Ejecutá CBMC sobre él. ¿Todo está en orden?
  3. Vas a observar que hay un bucle en la función boucle. El comportamiento de CBMC es de desarrollar completamente el bucle para generar sus restricciones. Acá logra hacerlo (es un bucle finito en este contexto), pero no siempre es el caso. Podés limitar el desarrollo con la opción --unwind n. Ejecutá cbmc boucle.c --unwind 3. ¿Qué ocurre? ¿Porqué?
  4. El test anterior no reportó ningun error porque las aserciones nunca son alcanzadas dentro de 3 iteraciones. De hecho, CBMC es capaz de detectar eso con la opción --unwinding-assertions. Ejecutá cbmc boucle.c --unwind 3 --unwinding-assertions. ¿Qué ocurre? ¿Para qué valor de unwind obtenés el comportamiento deseado?
  5. CBMC también es capaz de verificar solo partes de un código gracias a la opción --function. En ese caso, va a fijar el punto de entrada en la función que pasás como argumento. Ejecutá cbmc boucle.c --function boucle. ¿Qué ocurre?
  6. Hacelo de vuelta, pero usá la opción --unwind. ¿Es mejor?
  7. Ahora agregá la opción --unwinding-assertions. ¿Funciona? ¿Porqué? ¿Podés encontrar un valor de unwind para lo cual funciona?
  8. Si utilizás __CPROVER_assume, ¿podés tener una verificación exitosa?

Ejercicio 6: un bucle finito

  1. Bajá este código, e intentá verificarlo.
  2. ¿Podés encontrar un valor de unwind para lo cual la verificación es exitosa y ningun comportamiento se escapa (es decir --unwinding-assertions no produce ninguna falla)?

Ejercicio 7: asignación de memoria (facultativo)

  1. Considerá este programa. Verificalo con la opción --pointer-check. ¿Porqué hay un error? ¿Podés poner una restricción sobre n tal que la verificación sea exitosa?
  2. Ahora considerá este. Verificalo. ¿Qué pasa?

Ejercicio 8: Buffer overflow (facultativo)

  1. Considerá este programa. Verificá la función queue_test. ¿Hay un error? No te olvides de las opciones --bounds-check y --pointer-check.
  2. ¿Podés modificar el programa para hacer desaparecer esos errores?
  3. Incluso así, ¿tu programa no va a perder alguna información? Elaborá una manera de verificarlo con CBMC (usando aserciones).
  4. Una vez que está hecho, tratá de modificar tu programa para que se cumplan esas aserciones (quejándose o levantando una excepción cuando ocurra la pérdida de información).

Observaciones

Verificá la versión de CBMC que tenés instalada ejecutando cbmc sin opciones ni archicos.

Si tu versión es 5.6, cbmc no muestra los contraejemplos (si hay) por defecto, hay que darle la opción --trace.

Fuente de esta página