En clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentando las soluciones de los ejercicios de la 10ª relación, sobre árboles binarios.
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2014: Ejercicios sobre árboles binarios en Haskell”
En la clase anterior y en la de hoy del curso Lógica Informática se ha completado el estudio de la semántica de la lógica de primer orden introduciendo los conceptos de consistencia, consecuencia lógica y equivalencia. Se ha explicado la metodología de búqueda semántica de modelos y contramodelos.
Las transparencias de esta clase son las páginas 35 a 45 del tema 7:
Read More “LI2014: Semántica de la lógica de primer orden”
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í.