Mostrando las entradas con la etiqueta seguridad. Mostrar todas las entradas
Mostrando las entradas con la etiqueta seguridad. Mostrar todas las entradas

martes, 27 de mayo de 2025

Las buenas maneras de las llamadas recursivas

The Power of 10 Rules (El poder de las 10 reglas) es una guía para código seguro creada en 2006 por Gerard J. Holzmann del Laboratorio de Software Fiable de la NASA/JPL.

Las reglas prohíben ciertas prácticas de codificación en C que dificultan la revisión o el análisis estático del código. Estas reglas son un complemento a las directrices MISRA C y se han incorporado en el mayor conjunto de estándares de codificación de JPL.

Las diez reglas

  1. Restrinja todo el código a construcciones de flujo de control muy simples. No utilice sentencias GOTO, construcciones set jmp o long jmp, ni recursividad directa o indirecta.
  2. Todos los bucles deben tener un límite superior fijo. Debe ser trivialmente posible para una herramienta de comprobación demostrar estáticamente que no se puede superar un límite superior preestablecido en el número de iteraciones de un bucle. Si el límite del bucle no puede demostrarse estáticamente, se considera que se ha infringido la norma.
  3. No utilice la asignación dinámica de memoria después de la inicialización.
  4. Ninguna función debe ser más larga de lo que se puede imprimir en una sola hoja de papel.
  5. Use un mínimo de dos aserciones en tiempo de ejecución por función. Las aserciones siempre deben estar libres de efectos secundarios y deben definirse como pruebas booleanas.
  6. El scope de los datos debe ser el más pequeño posible.
  7. Cada función de llamada debe comprobar los valores de retorno de función no vacíos, y la validez de los parámetros debe comprobarse dentro de cada función.
  8. El uso del preprocesador debe limitarse a los headers y definiciones de macros simples.
  9. El uso de punteros debe estar restringido a un nivel de des referencia. No se permiten punteros a funciones.
  10. Todo el código debe ser compilado, desde el primer día de desarrollo, con todas las advertencias del compilador habilitadas en la configuración más estricta del compilador. Todo el código debe ser comprobado diariamente con al menos un analizador estático de código fuente actualizado, y debe pasar los análisis con cero advertencias.

La primera regla prohíbe el uso de llamadas recursivas. Las normas de la NASA se centran en la robustez de sistemas de tiempo real que son siempre críticos y inaccesibles para mantenimiento: La recursión puede ser impredecible en sistemas embebidos o de tiempo real.El consumo de recursos no acotados (pila/stack), es crítico en hardware con memoria limitada (ej.: satélites, rovers). Dificultad para verificación formal (requerida en software de seguridad crítica).

Recursión Eficiente: Optimización del Compilador

Para hacer que la recursión sea eficiente y segura, los compiladores modernos aplican optimizaciones clave, pero requieren que el código cumpla ciertas condiciones.

Tail-Call Optimization (TCO)

El compilador reemplaza la llamada recursiva por un bucle (jump) si la recursión está en posición de cola (tail position), evitando crecimiento de la pila (stack). La llamada recursiva debe ser la última operación de la función. Compiladores como GCC/Clang la optimizan con -O2 o -O3.

Trampolining (para lenguajes sin TCO nativo)

Transforma la recursión en un bucle usando una estructura intermedia ("trampolín").

Memoization (Cache de Resultados)

Almacena resultados previos para evitar recalcular en recursión múltiple.

Conversión Manual a Iteración

Si el compilador no optimiza, transforma la recursión en un bucle manualmente.

Fuentes:

NASA JPL Institutional Coding Standard for the C Programming Language (2009).

DO-178C (Estándar para software aeronáutico).

Resumen y extractos en el repositorio técnico de la NASA: NASA Technical Reports Server (NTRS) (Busca "JPL C Coding Standard 2009")

Versión similar y pública (JPL Power of Ten Rules): NASA JPL Power of 10 Rules (Reglas clave resumidas).

DO-178C (Estándar para Software Aeronáutico) Documento oficial: Publicado por RTCA (Requiere compra): RTCA DO-178C (Costo aproximado: $200 USD).

Guías gratuitas relacionadas:

FAA Advisory Circular 20-115C (basado en DO-178C): FAA.gov (Busca "AC 20-115C"). 

martes, 20 de mayo de 2025

Automatización de Pruebas Matemáticas

Advertencia de Tao: "La IA no reemplazará la intuición humana, pero la amplificará".

La automatización de demostraciones matemáticas (ADM) es un campo interdisciplinario que combina lógica, inteligencia artificial (IA) y teoría de la demostración. Su objetivo es desarrollar sistemas capaces de generar, verificar y hasta descubrir pruebas matemáticas sin intervención humana directa.

Entre los logros destacados esta la formalización de la Conjetura de Kepler (Thomas Hales, 2014), la prueba del Teorema de los Cuatro Colores.

El desafíos clave es la complejidad computacional. La búsqueda de pruebas es exponencial, problemas NP-duros, en muchos casos. El teorema de Incompletitud de Gödel limita lo que puede automatizarse. Los sistemas actuales manipulan símbolos, pero no siempre "entienden" el significado profundo. Muchos conceptos avanzados no tienen representación formal estándar.

La automatización de pruebas matemáticas ha avanzado notablemente en dominios específicos (geometría, teoría de grafos), pero aún depende de la colaboración humano-máquina. Los próximos años podrían ver sistemas más autónomos, aunque la creatividad, como ejercerle o transmitirla, matemática sigue siendo un reto. Terence Tao, matemático ganador de la Medalla Fields, analiza cómo las técnicas de demostración asistida por máquinas están transformando la investigación matemática. Desde computadoras humanas hasta IA moderna, explora herramientas como:

  • Resolvedores SAT (para problemas de lógica).
  • Asistentes de prueba formal (Coq, Lean).
  • Algoritmos de aprendizaje automático (como AlphaGeometry).

Tao destaca el potencial de combinar estas tecnologías para:

  • Colaboración a gran escala (ej.: proyectos colaborativos como Mathlib en Lean).
  • Explorar problemas complejos que humanos solos no podrían abordar.
  • Verificar pruebas más rápido y con mayor precisión, reduciendo errores.
El 25% de las pruebas en arxiv.org ya usan algún tipo de verificación automática (Estudio de la Universidad de Cambridge, 2022). Terence Tao Tao propone 3 escenarios para el 2030:
  1. Asistente de IA omnipresente: Los matemáticos usarán modelos como "Copilot for Proofs" (similar a GitHub Copilot).
  2. Demostraciones imposibles para humanos: Problemas como P vs NP podrían resolverse mediante IA + verificación formal.
  3. Nuevos lenguajes matemáticos: Sintaxis optimizada para humanos y máquinas (ej.: MathLang).

viernes, 16 de mayo de 2025

Peor es mejor

El artículo "Lisp: Good News, Bad News, How to Win Big" (Richard P. Gabriel, 1991), escrito en los años 90 por uno de los pioneros de LISP, durante el declive comercial de Lisp frente a lenguajes como C++ y Java, analiza por qué Lisp, pese a su elegancia técnica, no triunfó en la industria.

Gabriel muestra como Lisp es el lenguaje más potente (meta programación, macros, REPL); favorece abstracción pura y rapidez de desarrollo (ej.: IA simbólica). Gabriel critica la cultura UNIX/C por priorizar simplicidad sobre corrección, pero admite que eso las hizo más populares.

La sintaxis con paréntesis y la flexibilidad extrema de LISP asustaban a los desarrolladores. Los dialectos (Common Lisp vs. Scheme) fragmentaron el ecosistema. Lisp requería máquinas costosas (Lisp Machines) y no se adaptó a la era PC. Gabriel termina advirtiendo que la superioridad técnica no garantiza el éxito comercial.

Actualmente, ya en el segundo cuarto del siglo XXI, la IA permite meta programación implícita, es decir generar código desde descripciones en lenguaje natural). Asistentes como ChatGPT actúan como "REPLs cognitivos". La IA reduce la barrera de entrada, se afirma que ya no se requiere saber programar. Pero la ambigüedad es un problema fundamental que compromete la confiabilidad de los sistemas o aplicaciones desarrolladas por o con la asistencia de IA.

El ensayo de Edsger W. Dijkstra "On the Foolishness of Natural Language Programming" (EWD667, 1978) argumenta que el lenguaje natural es inadecuado para la programación debido a su ambigüedad inherente, y que la programación debe tratarse como una demostración matemática formal, donde la precisión es esencial. La ambigüedad del lenguaje natural lo hace propenso a malinterpretaciones, lo que es catastrófico en programación. La corrección del software solo puede garantizarse mediante pruebas formales (como en matemáticas), no mediante descripciones informales. Dijkstra criticaba los intentos de "programación en lenguaje natural" de su época, COBOL, por generar código inseguro y difícil de verificar.

El término "alucinaciones" en el contexto de la IA se refiere a situaciones en las que un modelo genera respuestas factualmente incorrectas o, específicamente en programación, código sintácticamente válido pero lógicamente erróneo (por ejemplo, un algoritmo de ordenación que no ordena correctamente). El término es ampliamente aceptado en la literatura (ej: estudios de OpenAI, DeepMind y MIT). Se aplica tanto a respuestas incorrectas como a código mal generado (Sutskever et al., 2023).

La IA genera código a partir de descripciones en lenguaje natural, lo que reproduce el problema de ambigüedad que Dijkstra señaló en sus críticas a la programación basada en lenguaje natural. Los modelos de lenguaje de gran escala (LLM, por sus siglas en inglés) no construyen demostraciones matemáticas del código ni verifican su corrección formal; en cambio, predicen secuencias de tokens basándose en patrones estadísticos aprendidos de su corpus de entrenamiento. Estos modelos no "comprenden" el código en un sentido lógico o semántico, sino que imitan estructuras recurrentes en los datos. Por lo tanto, no pueden garantizar la corrección del código generado, ya que carecen de razonamiento lógico formal (como los sistemas de tipos avanzados o demostradores de teoremas).los modelos LLM carecen de capacidad de verificación rigurosa más allá de la coherencia estadística. Su funcionamiento se basa en probabilidades, no en lógica deductiva (Bender et al., 2021). GitHub Copilot ha sugerido implementaciones de criptografía inseguras (estudio de NYU, 2022).

 Un modelo puede, por ejemplo,  generar un quicksort que funciona en el 90% de los casos, pero falla en edge cases (ej: listas vacías). La IA puede generar código con licencias conflictivas o soluciones sesgadas (ej: algoritmos de contratación discriminatorios). 

Alan Kay (Premio Turing): "La IA actual es como un loro que repite código sin comprenderlo. Necesitamos sistemas que razonen como humanos, no solo estadística."
Leslie Lamport (TLA+, Verificación Formal): "Los modelos generativos son útiles para prototipos, pero la corrección exige métodos formales."

Según un estudio del MIT (2023), solo el 40% del código generado por GPT-4 pasa pruebas formales de corrección. Google DeepMind (2024) propone combinar LLMs con *verificadores automáticos (ej: Lean, Coq).

En situaciones potencialmente catastróficas como la falla en un avión es esencial determinar quien es responsable. UE AI Act (2024) exige transparencia en sistemas de alto riesgo, pero no resuelve la verificación formal. Estamos entusiásticamente entrando en un proceso de automatización de errores: Si la IA escala la generación de código incorrecto, ¿aumentarán los desastres por software defectuoso? Si los programadores confían ciegamente en la IA, ¿se perderá el pensamiento crítico?

Dijkstra acertó en que el lenguaje natural es ambiguo y la programación exige precisión. La IA generativa agrava el problema, pues escala la generación de código no verificado. El futuro requiere modelos híbridos (IA + verificadores formales) y nuevos marcos legales para responsabilidad en código generado. Es necesario entrenar a los programadores en pensamiento crítico para que no deleguen ciegamente en la IA. La tecnología no triunfa solo por ser superior, sino por resolver problemas reales de manera accesible.

Lecturas clave:

Dijkstra, EWD667 (1978).

"Formal Verification in the Age of AI" (Communications of the ACM, 2024).

"Who is Liable for AI-Generated Bugs?" (Stanford Law Review, 2023).

miércoles, 24 de febrero de 2016

ISO/IEC 27001


ISO/IEC 27001 es un estándar para la seguridad de la información (Information technology - Security techniques - Information security management systems - Requirements) aprobado y publicado como estándar internacional en octubre de 2005 por International Organization for Standardization y por la comisión International Electrotechnical Commission.

Especifica los requisitos necesarios para establecer, implantar, mantener y mejorar un sistema de gestión de la seguridad de la información (SGSI) según el conocido como “Ciclo de Deming”: PDCA - acrónimo de Plan, Do, Check, Act (Planificar, Hacer, Verificar, Actuar). Es consistente con las mejores prácticas descritas en ISO/IEC 27002, anteriormente conocida como ISO/IEC 17799, con orígenes en la norma BS 7799-2:2002, desarrollada por la entidad de normalización británica, la British Standards Institution(BSI).

domingo, 7 de septiembre de 2014

Ariane 5

El 4 de junio de 1996, el cohete Ariane 5 lanzado por la Agencia Espacial Europea estalló 38 segundos después de su despegue desde Kourou, en la Guayana Francesa. El Ariane explotó en su primer viaje, después de una década de desarrollo, y las pérdidas se estimaron en 500 millones de dólares.

La causa de la explosión fue un error en el software. Un error no detectado por falta de control de la calidad del software crítico del cohete. Todo sucedió porque un número real de 64 bits (coma flotante) relacionado con la velocidad horizontal del cohete se convirtió en un entero de 16 bits. Ese mismo año, en 1996, a Alain Deutsch, del INRIA, le encargaron averiguar cuál fue el error. Y para ello se puso manos a la obra usando herramientas que automatizaban el control de la calidad del software crítico. Concretamente, usó un prototipo de analizador estático (IABC) de código fuente Ada, el cual había desarrollado para su doctorado.

Automatizando la evaluación de la calidad del software crítico, del código fuente, encontró el error,  y demostró la eficacia del análisis estático (os dejo un artículo para más detalles). Hoy en día el análisis estático del código es práctica usual, y prácticamente obligatoria, para controlar la calidad del software crítico, y del software embebido. Fue a raíz de esta experiencia cuando se creó la empresa PolySpace, con el objetivo de comercializar la herramienta de evaluación de la calidad del software crítico que se utilizó para encontrar el fallo del Ariane. Y hoy las herramientas de PolySpace son unas de las más usadas para el control de la calidad del software crítico.

miércoles, 11 de junio de 2014

código de barras invisible compuesto por nanopartículas

Un equipo del Worcester Polytechnic Institute han desarrollado una especie de código de barras invisible compuesto por nanopartículas que sobre el papel permitirían identificar y hacer un seguimiento de cualquier objeto sin que nadie sea consciente de ello.

técnica para identificar objetos de forma única

El proceso se realiza de forma íntegra en la fase de fabricación o composición del objeto a trazar, y sería indetectable a la vista. La identificación de la información que almacenan estos códigos se realizaría con un escáner capaz de leer el diferente punto de fusión de estas nanopartículas y que le otorgarían una huella única. Para conseguir una variedad adecuada de identificadores, las nanopartículas pueden combinarse sin problemas en busca de diferentes puntos de fusión.
Las primeras pruebas se están realizando con explosivos, medicinas, papel o incluso tinta, pero las posibilidades son muy amplias debido al tamaño ínfimo de las nanopartículas empleadas. En el caso de medicinas o alimentos, esas nanopartículas pueden ser orgánicas e incluso adecuadas para su ingesta.
Nanopartículas como ADN
Un elemento diferenciador de esta técnica respecto a otros desarrollos similares, principalmente basados en RFID, es la permanencia de esas nanopartículas incluso en condiciones como una explosión.
Las nanopartículas escogidas en este caso no reaccionarían en esa explosión gracias a que irían protegidas en cápsulas del tamaño de 200 nm, por lo que los desarrolladores afirman que incluso tras la detonación de una bomba, su técnica sería capaz de identificar el origen del explosivo.
Lo mismo se podría hacer con medicinas o dinero negro, apuntando por ahora la técnica a evitar delitos principalmente.
Vía | BBC. Más información | Nature.

jueves, 5 de junio de 2014

robo de un teléfono móvil

Qué hacer ante el robo de un teléfono móvil o una tableta

Con la ayuda de las aplicaciones de seguridad que ofrecen los fabricantes, los usuarios pueden rastrear la ubicación de un dispositivo; los consejos de un especialista de la Policía Metropolitana sobre cómo actuar en estos casos
Por   | LA NACION

Estos servicios no tienen costo y son muy fáciles de usar. Pero si el smartphone robado no está conectado a Internet o ya fue formateado, sólo se podrá ver su última ubicación conocida.
Para computadoras personales, una opción interesante es Prey Project , de código abierto y que admite teléfonos y tabletas con iOS o Android, además de equipos con Linux, Mac OS y Windows. Se pueden monitorear hasta tres equipos sin costo.
Las herramientas oficiales:

miércoles, 28 de mayo de 2014

Natas; Crónica del virus mexicano


En 1992 Little Loc se registro en Prodigy para buscar información sobre virii. Little Loc, alias James Gentile, a los 16 años había escrito un virus mutante que se dispersaba rápidamente. El virus, Satan Bug, estaba escrito de manera que el proceso mismo de rastrear un disco en busca de infección infectaba todos los ejecutables en el mismo.

Stuxnet

Israel y Estados Unidos desarrollaron técnicas para atacar sistemas de control industrial con el propósito de fastidiar a Irán,pero el secreto es saber que se puede y ahora el genio se salio de la lampara


viernes, 13 de septiembre de 2013

El gobierno uruguayo utilizar software libre en la administración pública

El gobierno uruguayo eligió utilizar software libre en la administración pública para disponer de un "comunicación segura" tras los recientes casos de espionaje por parte de los Estados Unidos, según anunció el canciller de ese país, Luis Almagro.

A medidados de julio, los presidentes de los países del Mercosur explicitaron en Montevideo la importancia de apoyar el desarrollo de software libre "a fin de lograr una verdadera apropiación, promoción del libre conocimiento y transferencia tecnológica, reduciendo la dependencia de soluciones provistas por trasnacionales del sector".

sábado, 17 de agosto de 2013

El precio de lo gratuito



La web parece estar desafiando todo el sentido económico que conocemos. Si el acceso a la mayoría de los sitios web es gratuito, ¿qué consiguen a cambio todas las empresas que gastan fortunas en sus sitios web? En este nuevo negocio de la información la moneda de cambio, no es tanto el dinero físico como los datos y características del usuario potencial del entorno web.

Así vemos como nuestra privacidad se diluye, se trafica con ella, en favor de los intereses económicos de las grandes empresas virtuales. En este episodio nos aproximaremos al afán de los anunciantes por descubrir lo que tecleamos en Google y lo que estarían dispuestos a pagar por influir en el resultado de lo que vemos cuando pulsamos 'Buscar'. Sin embargo, Google está dirigiéndose hacia el desarrollo de redes sociales como Facebook que requieren de claves de acceso. ¿Se convertirán estas redes invisibles en una web paralela?.

martes, 14 de mayo de 2013

domingo, 18 de septiembre de 2011

QR codes

A QR code (abbreviated from Quick Response code) is a type of matrix barcode (or two-dimensional code) first designed for the automotive industry. More recently, the system has become popular outside of industry due to its fast readability and comparatively large storage capacity. The code consists of black modules arranged in a square pattern on a white background. The information encoded can be made up of any kind of data (e.g., binary, alphanumeric, or Kanji symbols)[1]
Malicious QR codes combined with a permissive reader can put a computer's contents and user's privacy at risk. QR codes intentionally obscure and compress their contents and intent to humans.[19]They are easily created and may be affixed over legitimate QR codes.[20] On a smartphone, the reader's many permissions may allow use of the camera, full internet access, read/write contact data,GPS, read browser history, read/write local storage, and global system changes.[21][22][23]
Risks include linking to dangerous websites with browser exploits, enabling the microphone/camera/GPS and then streaming those feeds to a remote server, exfiltrating senstive data (passwords, files, contacts, transactions),[24] and sending email/SMS/IM messages or DDOS packets as part of a botnet, corrupting privacy settings, stealing identity,[25] and even containing malicious logic themselves such as JavaScript[26] or a virus.[27][28] These actions may occur in the background while the user only sees the reader opening a harmless webpage. [29]

miércoles, 29 de julio de 2009

El bueno, malo, y bonito

javascript esta en un estado límbico. Por un lado permite trucos de manejo de pantallas tipo Ajax y por otro es un riesgo de seguridad. ¿Qué influencia será más fuerte?

Firefox flaws raise Mozilla security doubts

ASP.Net Security

tecnologias ASP.Net Make sure you are very familiar with the following terms:
  • Authentication. Positively identifying the clients of your application; clients might include end-users, services, processes or computers.
  • Authorization. Defining what authenticated clients are allowed to see and do within the application.
  • Secure Communications. Ensuring that messages remain private and unaltered as they cross networks.
  • Impersonation. This is the technique used by a server application to access resources on behalf of a client. The client's security context is used for access checks performed by the server.
  • Delegation. An extended form of impersonation that allows a server process that is performing work on behalf of a client, to access resources on a remote computer. This capability is natively provided by Kerberos on Microsoft® Windows® 2000 and later operating systems. Conventional impersonation (for example, that provided by NTLM) allows only a single network hop. When NTLM impersonation is used, the one hop is used between the client and server computers, restricting the server to local resource access while impersonating.
  • Security Context. Security context is a generic term used to refer to the collection of security settings that affect the security-related behavior of a process or thread. The attributes from a process' logon session and access token combine to form the security context of the process.
  • Identity. Identity refers to a characteristic of a user or service that can uniquely identify it. For example, this is often a display name, which often takes the form authority/user name.

Principles

There are a number of overarching principles that apply to the guidance. The following summarizes these principles:
  • Adopt the principle of least privilege. Processes that run script or execute code should run under a least privileged account to limit the potential damage that can be done if the process is compromised. If a malicious user manages to inject code into a server process, the privileges granted to that process determine to a large degree the types of operations the user is able to perform. Code that requires additional trust (and raised privileges) should be isolated within separate processes.The ASP.NET team made a conscious decision to run the ASP.NET account with least privileges.
  • Use defense in depth. Place check points within each of the layers and subsystems within your application. The check points are the gatekeepers that ensure that only authenticated and authorized users are able to access the next downstream layer.
  • Don't trust user input. Applications should thoroughly validate all user input before performing operations with that input. The validation may include filtering out special characters. This preventive measure protects the application against accidental misuse or deliberate attacks by people who are attempting to inject malicious commands into the system. Common examples include SQL injection attacks, cross-site scripting attacks, and buffer overflow.
  • Use secure defaults. A common practice among developers is to use reduced security settings, simply to make an application work. If your application demands features that force you to reduce or change default security settings, test the effects and understand the implications before making the change.
  • Don't rely on security by obscurity. Trying to hide secrets by using misleading variable names or storing them in odd file locations does not provide security. In a game of hide-and-seek, it's better to use platform features or proven techniques for securing your data.
  • Check at the gate. You don't always need to flow a user's security context to the back end for authorization checks. Often, in a distributed system, this is not the best choice. Checking the client at the gate refers to authorizing the user at the first point of authentication (for example, within the Web application on the Web server), and determining which resources and operations (potentially provided by downstream services) the user should be allowed to access.If you design solid authentication and authorization strategies at the gate, you can circumvent the need to delegate the original caller's security context all the way through to your application's data tier.
  • Assume external systems are insecure. If you don't own it, don't assume security is taken care of for you.
  • Reduce surface area. Avoid exposing information that is not required. By doing so, you are potentially opening doors that can lead to additional vulnerabilities. Also, handle errors gracefully; don't expose any more information than is required when returning an error message to the end user.
  • Fail to a secure mode. If your application fails, make sure it does not leave sensitive data unprotected. Also, do not provide too much detail in error messages; meaning don't include details that could help an attacker exploit a vulnerability in your application. Write detailed error information to the Windows event log.
  • Remember you are only as secure as your weakest link. Security is a concern across all of your application tiers.
  • If you don't use it, disable it. You can remove potential points of attack by disabling modules and components that your application does not require. For example, if your application doesn't use output caching, then you should disable the ASP.NET output cache module. If a future security vulnerability is found in the module, your application is not threatened.
The following steps identify a process that will help you develop an authentication and authorization strategy for your application:
  1. Identify resources
  2. Choose an authorization strategy
  3. Choose the identities used for resource access
  4. Consider identity flow
  5. Choose an authentication approach
  6. Decide how to flow identity
Building Secure ASP.NET Applications: Authentication, Authorization, and Secure Communication