@prefix prodottidellaricerca: . @prefix istituto: . @prefix prodotto: . istituto:CDS044 prodottidellaricerca:prodotto prodotto:ID64139 . @prefix pubblicazioni: . @prefix unitaDiPersonaleInterno: . unitaDiPersonaleInterno:MATRICOLA7856 pubblicazioni:autoreCNRDi prodotto:ID64139 . @prefix modulo: . modulo:ID2828 prodottidellaricerca:prodotto prodotto:ID64139 . unitaDiPersonaleInterno:MATRICOLA11430 pubblicazioni:autoreCNRDi prodotto:ID64139 . @prefix rdf: . prodotto:ID64139 rdf:type prodotto:TIPO1101 . @prefix retescientifica: . prodotto:ID64139 rdf:type retescientifica:ProdottoDellaRicerca . @prefix rdfs: . prodotto:ID64139 rdfs:label "A framework for automatic generation of security controller (Articolo in rivista)"@en . @prefix xsd: . prodotto:ID64139 pubblicazioni:anno "2010-01-01T00:00:00+01:00"^^xsd:gYear ; pubblicazioni:doi "10.1002/stvr.441"^^xsd:string . @prefix skos: . prodotto:ID64139 skos:altLabel "
Martinelli F.; Matteucci I. (2010)
A framework for automatic generation of security controller
in Software testing, verification & reliability
"^^rdf:HTML ; pubblicazioni:autori "Martinelli F.; Matteucci I."^^xsd:string . @prefix ns11: . prodotto:ID64139 pubblicazioni:rivista ns11:ID251008 ; pubblicazioni:note "In: Software Testing, Verification & Reliability (STVR) Journal, vol. on-line article n. n/a. John Wiley & Sons, Ltd, 2010."^^xsd:string ; skos:note "Google Scholar"^^xsd:string ; pubblicazioni:affiliazioni "CNR-IIT, Pisa"^^xsd:string ; pubblicazioni:titolo "A framework for automatic generation of security controller"^^xsd:string ; prodottidellaricerca:abstract "This paper concerns the study, the development and the synthesis of mechanisms for guaranteeing the security of complex systems, i.e., systems composed by several interactive components. A complex system under analysis is described as an open system, in which a certain component has an unspecified behavior (not fixed in advance). Regardless of the unspecified behavior, the system should work properly, e.g., should satisfy a certain property. Within this formal approach, we propose techniques to enforce properties and synthesize controller programs able to guarantee that, for all possible behaviors of the unspecified component, the overall system results secure. For performing this task, we use techniques able to provide us necessary and sufficient conditions on the behavior of this unspecified component to ensure the whole system is secure. Hence, we automatically synthesize the appropriate controller programs by exploiting satisfiability results for temporal logic. We contribute within the area of the enforcement of security properties by proposing a flexible and automated framework that goes beyond the definition of how a system should behave to work properly. Indeed, while the majority of related work focuses on the definition of monitoring mechanisms, we aid in the synthesis of enforcing techniques. Moreover, we present a tool for the synthesis of secure systems able to generate a controller program directly executable on real devices as smart phone"@en ; prodottidellaricerca:prodottoDi modulo:ID2828 , istituto:CDS044 ; pubblicazioni:autoreCNR unitaDiPersonaleInterno:MATRICOLA11430 , unitaDiPersonaleInterno:MATRICOLA7856 . @prefix parolechiave: . prodotto:ID64139 parolechiave:insiemeDiParoleChiave . ns11:ID251008 pubblicazioni:rivistaDi prodotto:ID64139 . parolechiave:insiemeDiParoleChiaveDi prodotto:ID64139 .