View
847
Download
1
Category
Preview:
DESCRIPTION
Uma implementação de LDAP em VDM++
Citation preview
LDAP em VDM++
Pedro Pereira Ulisses Costa
Metodos Formais em Engenharia de Software
12 de Fevereiro de 2009
Pedro Pereira, Ulisses Costa LDAP em VDM++
Sumario
1 LDAPO que e o LDAP e a DITEstrutura do LDAPPropriedades do LDAP
2 VDMDIT - Tree? & ForestServidor
3 Operacoes do Servidor
Pedro Pereira, Ulisses Costa LDAP em VDM++
Sumario
1 LDAPO que e o LDAP e a DITEstrutura do LDAPPropriedades do LDAP
2 VDMDIT - Tree? & ForestServidor
3 Operacoes do Servidor
Pedro Pereira, Ulisses Costa LDAP em VDM++
LDAP
LDAP vs DAP - Lightweight porque opera em TCP/IP
LDAP e pelo menos uma DIT
Uma directoria e uma maneira de organizar informacaocomplexa, tornando facil a sua pesquisa.
Pedro Pereira, Ulisses Costa LDAP em VDM++
Sumario
1 LDAPO que e o LDAP e a DITEstrutura do LDAPPropriedades do LDAP
2 VDMDIT - Tree? & ForestServidor
3 Operacoes do Servidor
Pedro Pereira, Ulisses Costa LDAP em VDM++
Estrutura da DIT
Funcao da DIT
Guardar a hierarquia
Composta por entradas
Entradas sao instancias de ObjectClass
ObjectClass’s podem ter atributos
Atributos relacionam a informacao
Pedro Pereira, Ulisses Costa LDAP em VDM++
Estrutura das entradas
Contem uma instancia de ObjectClass
Atributos obrigatorios da ObjectClass
Um DN (Distinguished Name))
Unico em toda a arvore
Um RDN (Relative Distinguished Name)
Unico entre irmaos
Pedro Pereira, Ulisses Costa LDAP em VDM++
Sumario
1 LDAPO que e o LDAP e a DITEstrutura do LDAPPropriedades do LDAP
2 VDMDIT - Tree? & ForestServidor
3 Operacoes do Servidor
Pedro Pereira, Ulisses Costa LDAP em VDM++
Propriedades do LDAP
Floresta de DIT’s
DN’s sao unicos na DIT
Um DN e: O DN do antecessor e o seu RDN
Cada atributo tem pares de (identificador,valor)
Pedro Pereira, Ulisses Costa LDAP em VDM++
Sumario
1 LDAPO que e o LDAP e a DITEstrutura do LDAPPropriedades do LDAP
2 VDMDIT - Tree? & ForestServidor
3 Operacoes do Servidor
Pedro Pereira, Ulisses Costa LDAP em VDM++
Sumario
1 LDAPO que e o LDAP e a DITEstrutura do LDAPPropriedades do LDAP
2 VDMDIT - Tree? & ForestServidor
3 Operacoes do Servidor
Pedro Pereira, Ulisses Costa LDAP em VDM++
DIT - Tree?
Grafo acıclico e ligado (uma raız)
The root of the DIT is a DSA-specific Entry (DSE) and notpart of any naming context
Pedro Pereira, Ulisses Costa LDAP em VDM++
DIT - Forest
Grafo acıclico e nao ligado (multiplas raızes)
Pedro Pereira, Ulisses Costa LDAP em VDM++
Sumario
1 LDAPO que e o LDAP e a DITEstrutura do LDAPPropriedades do LDAP
2 VDMDIT - Tree? & ForestServidor
3 Operacoes do Servidor
Pedro Pereira, Ulisses Costa LDAP em VDM++
Servidor Estrutura
class Server
types
public String = seq of char;
public OName = String;
public AName = String;
public Value = String;
public ObjClass :: must : set of AName
may : set of AName;
instance variables
private entries : map nat1 to Entry; -- entradas existentesprivate dit : map nat1 to set of nat1; -- hierarquia das entradasprivate def_objs : map OName to ObjClass; -- objectos definidosprivate def_attrs : set of AName; -- atributos definidos
inv ServerINV ();
Pedro Pereira, Ulisses Costa LDAP em VDM++
Servidor Invariantes
The root of the DIT is a DSA-specific Entry (DSE) and not part of any namingcontext;
Entries have names: one or more attribute values from the entry form its relativedistinguished name (RDN), which MUST be unique among all its siblings;
The concatenation of the relative distinguished names of the sequence of entriesfrom a particular entry to an immediate subordinate of the root of the treeforms that entry’s Distinguished Name (DN), which is unique in the tree;
Each entry MUST have an objectClass attribute which specifies the objectclasses of that entry ;
Servers MUST NOT permit clients to add attributes to an entry unless thoseattributes are permitted by the object class definitions, the schema controllingthat entry ;
Entries consist of a set of attributes;
An attribute is a type with one or more associated values and is identified by ashort descriptive name (...);
Schema is the collection of attribute type definitions, object class definitions andother information (...);
Pedro Pereira, Ulisses Costa LDAP em VDM++
Servidor Invariantes
public ServerINV: () ==> bool
ServerINV () ==
(
return (
-- dit aciclica( not exists e in set dom dit & e in set TransitiveClosure(e) ) and
-- todos os elementos que existem estao na dit( forall e in set ( dom dit union rng dit ) & e in set dom entries ) and
-- objectos apenas contem atributos definidos( forall o in set rng def_objs & ( forall a in set ( o.must union o.may
) & a in set def_attrs ) ) and
-- dn unico entre todos os elementos da floresta( forall e1, e2 in set rng entries & e1.GetDN() <> e2.GetDN () ) and
-- dn do pai contido no do filho( forall p in set dom dit & ( forall c in set TransitiveClosure(p) & (
elems entries(c).GetDN() ) subset ( elems entries(p).GetDN() ) ) )
and
-- rdn unico entre irmaos( forall p in set dom dit & ( forall c1, c2 in set dit(p) & entries(c1).
GetRDN () <> entries(c2).GetRDN () ) ) and
-- rdn faz parte do dn( forall e in set rng entries & e.GetRDN () in set elems e.GetDN () ) and
-- rdn composto por um atributo( forall e in set rng entries & e.GetRDN () in set dom e.GetAttrs () )));
Pedro Pereira, Ulisses Costa LDAP em VDM++
Sumario
1 LDAPO que e o LDAP e a DITEstrutura do LDAPPropriedades do LDAP
2 VDMDIT - Tree? & ForestServidor
3 Operacoes do Servidor
Pedro Pereira, Ulisses Costa LDAP em VDM++
Servidor Operacoes
CRUD
Create Read Update Delete
Add Entry
Del Entry
Modify DN
Search Entry
Search Attributes
Pedro Pereira, Ulisses Costa LDAP em VDM++
Modify DN
public ModDN: seq of AName * AName ==> ()
ModDN(old_dn , new_rdn) ==
(
dcl new_dn: seq of AName := [];
dcl pos: nat1 := len old_dn - 1;
dcl e: nat1 := GetID(old_dn);
for i = 1 to pos do
new_dn := new_dn ^ [old_dn(i)];
new_dn := new_dn ^ [new_rdn ];
entries(e).SetDN(new_dn);
for all c in set TransitiveClosure(e) do
(
new_dn := [];
for i = 1 to ( len entries(c).GetDN () ) do
if i = pos
then new_dn := new_dn ^ [new_rdn]
else new_dn := new_dn ^ entries(c).GetDN ()(i);
entries(c).SetDN(new_dn);
);
)
pre ( exists i in set dom entries & entries(i).GetDN() = old_dn )
post ( exists i in set dom entries & forall c in set TransitiveClosure(i) &
new_rdn in set elems entries(i).GetDN() and new_rdn in set elems entries(c)
.GetDN() );
Pedro Pereira, Ulisses Costa LDAP em VDM++
GetID
public GetID: seq of AName ==> nat
GetID(dn) ==
(
for all i in set dom entries do
if entries(i).GetDN() = dn
then return i;
return 0;
)
post ( not exists i in set dom entries & entries(i).GetDN() = dn => RESULT = 0 )
or
( exists i in set dom entries & entries(i).GetDN() = dn => RESULT = i );
Pedro Pereira, Ulisses Costa LDAP em VDM++
Transitive Closure
public TransitiveClosure: nat1 ==> set of nat1
TransitiveClosure(origem) ==
(
dcl res: set of nat1 := {};
dcl childs: set of nat1 := dit(origem);
while childs <> {} do
(
for all c in set childs do
(
childs := childs union dit(c);
res := res union {c};
);
childs := childs \ res;
);
return res;
)
pre origem in set dom entries
post forall e in set RESULT & ( elems entries(origem).GetDN() ) subset ( elems
entries(e).GetDN() );
Pedro Pereira, Ulisses Costa LDAP em VDM++
Recommended