Reseña: The Unified Policy Framework (UPF)

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre seguridad titulado The Unified Policy Framework (UPF)

Sus autores son

Su resumen es

We present the Unified Policy Framework (UPF), a generic framework for modelling security (access-control) policies. UPF emphasizes the view that a policy is a policy decision function that grants or denies access to resources, permissions, etc. In other words, instead of modelling the relations of permitted or prohibited requests directly, we model the concrete function that implements the policy decision point in a system. In more detail, UPF is based on the following four principles: 1) Functional representation of policies, 2) No conflicts are possible, 3) Three-valued decision type (allow, deny, undefined), 4) Output type not containing the decision only.

El marco en el que se apoya el trabajo se presenta en la tesis de Lukas Brügger A framework for modelling and testing of security policies.

El trabajo se ha publicado en The Archive of Formal Proofs.

El código de las correspondientes teorías en Isabelle se encuentra aquí.

I1M2014: Definiciones de tipos y clases en Haskell

PorJosé A. Alonso

En clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la definición de nuevos tipos de datos y de funciones sobre dichos tipos. Concretamente, se ha visto

  • cómo definir tipos usando type,
  • cómo definir funciones con dominio o rango en tipos definidos usando type,
  • cómo definir tipos usando data,
  • cómo definir funciones con dominio o rango en tipos definidos usando data y
  • cómo definir tipos de datos recursivos usando como ejemplo los naturales, los árboles y las fórmulas proposicionales.

Como caso de estudio, se ha explicado cómo construir un programa para determinar si una fórmula es una tautología.

El código correspondiente es
Read More “I1M2014: Definiciones de tipos y clases en Haskell”

LI2014: Sintaxis y semántica de la lógica de primer orden

PorJosé A. Alonso

En la clase de hoy del curso de Lógica Informática se presentado la sintaxis y la semántica de la lógica de primer orden como respuestas a las siguientes preguntas: ¿qué es una fórmula?, ¿qué significa que una fórmula verdadera?

En primer lugar, a partir de los ejemplos de representación del conocimiento, se han definido los símbolos lógicos (variables, conectivas, cuantificadores e igualdad) y los símbolos no lógicos (constantes, predicados y funciones) que forman el alfabeto del lenguaje de la lógica de primer orden.

A partir del alfabeto, se definen los términos, las fórmulas atómicas y las fórmulas del lenguaje.

Como medio del reconocimiento de fórmulas, se introducen los árboles de análisis. Con ello, respondemos a la primera de las preguntas iniciales.

En el estudio sintáctico, definimos el conjunto de las subfórmulas, el conjunto de las variables de un término, las ocurrencias libres y ligadas, el conjunto de las variables libres y ligadas y las fómulas cerradas y abiertas. Algunas de las definiciones anteriores se realizan por recursión sobre fórmulas o sobre términos.

En segundo lugar hemos estudiado la semántica, comenzando con distintas cuestiones sobre qué significa que una fórmula sea verdadera para resaltar su dependencia del universo, la interpretación de los símbolos no lógico y de las asignaciones a las variables libres.

Se han definido las estructuras de un lenguaje, las asignaciones a las variables y las interpretaciones de un lenguaje.

Se ha definido el valor de un término o de una fórmula en una interpretación. Con ello, respondemos a la segunda de las preguntas iniciales.

Las transparencias de esta clase son las páginas 1 a 34 del tema 7:
Read More “LI2014: Sintaxis y semántica de la lógica de primer orden”