• Home
  • Química
  • Astronomía
  • Energía
  • Naturaleza
  • Biología
  • Física
  • Electrónica
  • Pruebas de verificación matemática si el software se ejecuta como se anuncia

    Crédito:CC0 Public Domain

    Cuando se trata de seguridad, lo que no sabes puede lastimarte.

    La mayoría de la gente nunca piensa en el cifrado que subyace a las actividades seguras en línea, incluida la banca, compras y comunicaciones. Pero todos se basan en programas informáticos para generar un número aleatorio que sirve como clave para desbloquear la comunicación cifrada. El problema es que pequeños errores de programación pueden hacer que estos sistemas sean vulnerables, y esas vulnerabilidades a menudo pueden ser muy difíciles de detectar.

    "Siempre que te conectes a Amazon para darles tu número de tarjeta de crédito, siempre que inicie sesión en algún lugar a través de una conexión segura, depende de claves criptográficas generadas aleatoriamente, "dijo Andrew Appel, el profesor Eugene Higgins de Ciencias de la Computación en Princeton. "Y si el adversario, el espía que intenta leer tus mensajes o hacerse pasar por ti, podría adivinar qué número aleatorio estaba usando su computadora, entonces podría saber qué clave vas a utilizar y podría hacerse pasar por tu tráfico y leer tus mensajes ".

    La investigación de Appel se ha centrado durante mucho tiempo en la intersección de la informática y las políticas públicas. Ha escrito extensamente sobre la tecnología de las máquinas de votación y ha testificado ante el Congreso sobre métodos para asegurar el sistema electoral de EE. UU. En un trabajo reciente, su investigación se ha centrado en la verificación formal, un conjunto de herramientas "para especificar qué deben hacer los programas, para la construcción de programas que se ajusten a esas especificaciones, y para verificar que los programas se comporten exactamente como se especifica, "según el sitio web de DeepSpec, un proyecto multiinstitucional que lidera Appel.

    En un ejemplo de verificación matemática de la corrección de una función crítica, El grupo de Appel desarrolló un método para verificar la fuerza de los generadores de números aleatorios que forman la base de la mayoría de los sistemas de cifrado. En un artículo que surgió del trabajo de tesis senior de Katherine Ye '16, el equipo (que también incluía investigadores de la Universidad Johns Hopkins y Oracle) examinó un generador de números aleatorios de uso común y produjo una prueba completa y comprobada por máquina de que el sistema es realmente seguro. Los métodos convencionales, como las pruebas exhaustivas, no pueden determinar si un generador de números aleatorios es seguro.

    Comentando el trabajo, Eugene Spafford, líder en seguridad y garantía de la información en Purdue University, dijo que la investigación es un avance significativo. "Como muchas otras investigaciones, puede que no se aplique directamente a tu vida y a la mía en este momento, pero está generando un conjunto de resultados que podrían [conducir a] resultados muy importantes en el futuro ".


    © Ciencia https://es.scienceaq.com