CCured

En este documento proponemos un esquema que combina la inferencia de tipos y la verificación en tiempo de ejecución para hacer que los programas C existentes sean seguros en cuanto a tipos. Describimos el sistema de tipos CCured, que extiende el de C al separar los tipos de punteros según su uso. Este sistema de tipos permite que tanto los punteros cuyo uso se puede verificar estáticamente sean seguros en cuanto a tipos, como los punteros cuya seguridad debe ser verificada en tiempo de ejecución. Demostramos un resultado de corrección de tipos y luego presentamos un sorprendentemente simple algoritmo de inferencia de tipos que es capaz de inferir los tipos de punteros apropiados para los programas C existentes. Nuestra experiencia con el sistema CCured muestra que la inferencia es muy efectiva para muchos programas C, ya que es capaz de inferir que la mayoría o todos los punteros son verificables estáticamente para ser seguros en cuanto a tipos. Los punteros restantes se instrumentan con verificaciones eficientes en tiempo de ejecución para asegurar que se utilicen de manera segura. La pérdida de rendimiento resultante debido a las verificaciones en tiempo de ejecución es del 0-150%, lo cual es varias veces mejor que los enfoques comparables que utilizan solo verificación dinámica. Usando CCured hemos descubierto errores de programación en programas C consolidados como varios benchmarks SPECINT95.