Bien, entonces la confianza se traslada del componente al comprobador de pruebas. ¿Sobre qué base se puede confiar en el proceso de certificación del verificador?
Se puede confiar en el proceso de certificación del verificador de pruebas porque:
- el verificador de pruebas define la política de seguridad;
- el verificador de pruebas emplea sus axiomas para validar el predicado de seguridad, y así sabe si el predicado de seguridad cumple las condiciones de la política de seguridad, o no;
- El comprobador de pruebas establece las reglas de generación de VC, las reglas de prueba y las condiciones previas (esencialmente la "convención de llamada") que define cómo el consumidor de código invoca los binarios.
Parece todo bien ¿verdad? Sin embargo, antes de que esto suceda, el consumidor de código define y publica su política de seguridad.
- ¿Las políticas de seguridad permanecen estáticas?
- ¿Son las políticas de seguridad, en cualquier momento, suficientes con sus reglas de generación de VC, reglas de prueba y condiciones previas para certificar que los predicados de seguridad realmente establecen un código no malicioso compatible?
- ¿Pueden los productores de código realmente certificar un predicado de seguridad usando lógica de primer orden en tiempo polinomial?
En el primer punto , si se encuentra que la política de seguridad es demasiado simplista o no tiene los axiomas adecuados, cambiará, lo que significa que se debe volver a escribir y volver a publicar, lo que significa que el código el productor debe volver a desarrollar un predicado de seguridad y una prueba de seguridad para la recertificación.
¿Qué productor de código (con la esperanza de que su código se reutilice en diferentes entornos) recreará constantemente predicados de seguridad y volverá a desarrollar pruebas de seguridad cada vez que cambie la política de seguridad de alguien, para cada escenario posible? El problema de la confianza es una restricción para el consumidor de código, no para el productor de código a quien no le importa si sus binarios son de confianza.
Al segundo punto ,
Para formular una política de seguridad, los consumidores del código deben hacer suposiciones sobre las condiciones suficientes para certificar un predicado de seguridad. El simple hecho de que un predicado de seguridad reciba la certificación, no significa que sea realmente seguro. Más bien, solo significa que ha cumplido con las condiciones mínimas necesarias impuestas por los consumidores del código; por lo tanto, un umbral mínimo de suficiencia que puede no ser suficiente para garantizar una seguridad real.
Si un consumidor de código construye y publica una política de seguridad ineficaz, el proceso de certificación no proporciona un control suficiente contra la ejecución de código malicioso. De hecho, este modelo tiene al productor de código abrogando su responsabilidad de escribir código confiable, a favor de escribir código que simplemente cumpla con las condiciones mínimas para la certificación (es decir, uno que produzca un predicado de seguridad mínimamente aceptable).
Finalmente, al tercer punto ,
El autor señala que "para crear una prueba de seguridad, el productor de código debe probar un predicado en la lógica de primer orden. En general, este problema es indecidible".
Si crear una prueba de seguridad requiere probar un predicado en la lógica de primer orden que es "en general" indecidible, esto implica que el productor del código no puede, en general, crear una prueba de seguridad. ¿De qué sirve la certificación en primer lugar? ¿No es todo meramente académico?
Hay otros problemas que los autores mencionan en la Introducción que " ... hay muchos problemas difíciles que quedan por resolver. " ¡De verdad!
RESPUESTA :
Usted pregunta ¿Hay alguna razón para que PCC no se use más ampliamente?
Parece que hay muy pocos incentivos por parte de los productores de código para utilizar más ampliamente este modelo, dada la batalla aparentemente imposible que enfrentan al crear una prueba de seguridad para su predicado y tener su el predicado de seguridad cumple las condiciones de algún proceso de certificación particular .