Visible to the public "Verification for Security-Relevant Properties and Hyperproperties"Conflict Detection Enabled

Title"Verification for Security-Relevant Properties and Hyperproperties"
Publication TypeConference Paper
Year of Publication2015
AuthorsT. Long, G. Yao
Conference Name2015 IEEE 12th Intl Conf on Ubiquitous Intelligence and Computing and 2015 IEEE 12th Intl Conf on Autonomic and Trusted Computing and 2015 IEEE 15th Intl Conf on Scalable Computing and Communications and Its Associated Workshops (UIC-ATC-ScalCom)
Date PublishedAug
ISBN Number 978-1-4673-7211-4
Accession Number16158405
KeywordsAccess Control, Computational modeling, data privacy, data privacy preservation, Embedded systems, fairness, hyperproperty, hyperproperty verification, liveness, model checking, privacy analysis, program verification, pubcrawl, pubcrawl170105, Safety, security policy, security-relevant properties, security-relevant property verification, Time factors, verification, Wireless sensor networks
Abstract

Privacy analysis is essential in the society. Data privacy preservation for access control, guaranteed service in wireless sensor networks are important parts. In programs' verification, we not only consider about these kinds of safety and liveness properties but some security policies like noninterference, and observational determinism which have been proposed as hyper properties. Fairness is widely applied in verification for concurrent systems, wireless sensor networks and embedded systems. This paper studies verification and analysis for proving security-relevant properties and hyper properties by proposing deductive proof rules under fairness requirements (constraints).

URLhttp://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7518280&isnumber=7518175
DOI10.1109/UIC-ATC-ScalCom-CBDCom-IoP.2015.101
Citation Key7518280