Bibliographies thématiques / Hyperproperties verification

Littérature scientifique sur le sujet « Hyperproperties verification »

Auteur : Grafiati
Publié le 11 mars 2023

Créez une référence correcte selon les styles APA, MLA, Chicago, Harvard et plusieurs autres

Choisissez une source :

Sommaire

Consultez les listes thématiques d’articles de revues, de livres, de thèses, de rapports de conférences et d’autres sources académiques sur le sujet « Hyperproperties verification ».

À côté de chaque source dans la liste de références il y a un bouton « Ajouter à la bibliographie ». Cliquez sur ce bouton, et nous générerons automatiquement la référence bibliographique pour la source choisie selon votre style de citation préféré : APA, MLA, Harvard, Vancouver, Chicago, etc.

Vous pouvez aussi télécharger le texte intégral de la publication scolaire au format pdf et consulter son résumé en ligne lorsque ces informations sont inclues dans les métadonnées.

Articles de revues sur le sujet "Hyperproperties verification"

1

Wang, Yu, Mojtaba Zarei, Borzoo Bonakdarpour et Miroslav Pajic. « Statistical Verification of Hyperproperties for Cyber-Physical Systems ». ACM Transactions on Embedded Computing Systems 18, no 5s (19 octobre 2019) : 1–23. http://dx.doi.org/10.1145/3358232.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
2

Finkbeiner, Bernd, Christopher Hahn, Marvin Stenger et Leander Tentrup. « Efficient monitoring of hyperproperties using prefix trees ». International Journal on Software Tools for Technology Transfer 22, no 6 (20 février 2020) : 729–40. http://dx.doi.org/10.1007/s10009-020-00552-5.

Texte intégral
Résumé :
Abstract Hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other and are thus not monitorable by tools that consider computations in isolation. We present the monitoring approach implemented in the latest version of $$\text {RVHyper}$$ RVHyper , a runtime verification tool for hyperproperties. The input to the tool are specifications given in the temporal logic $$\text {HyperLTL}$$ HyperLTL , which extends linear-time temporal logic (LTL) with trace quantifiers and trace variables. $$\text {RVHyper}$$ RVHyper processes execution traces sequentially until a violation of the specification is detected. In this case, a counterexample, in the form of a set of traces, is returned. $$\text {RVHyper}$$ RVHyper employs a range of optimizations: a preprocessing analysis of the specification and a procedure that minimizes the traces that need to be stored during the monitoring process. In this article, we introduce a novel trace storage technique that arranges the traces in a tree-like structure to exploit partially equal traces. We evaluate $$\text {RVHyper}$$ RVHyper on existing benchmarks on secure information flow control, error correcting codes, and symmetry in hardware designs. As an example application outside of security, we show how $$\text {RVHyper}$$ RVHyper can be used to detect spurious dependencies in hardware designs.
Styles APA, Harvard, Vancouver, ISO, etc.
3

Stucki, Sandro, César Sánchez, Gerardo Schneider et Borzoo Bonakdarpour. « Gray-box monitoring of hyperproperties with an application to privacy ». Formal Methods in System Design, 2 février 2021. http://dx.doi.org/10.1007/s10703-020-00358-w.

Texte intégral
Résumé :
AbstractRuntime verification is a complementary approach to testing, model checking and other static verification techniques to verify software properties. Monitorability characterizes what can be verified (monitored) at run time. Different definitions of monitorability have been given both for trace properties and for hyperproperties (properties defined over sets of traces), but these definitions usually cover only some aspects of what is important when characterizing the notion of monitorability. The first contribution of this paper is a refinement of classic notions of monitorability both for trace properties and hyperproperties, taking into account, among other things, the computability of the monitor. A second contribution of our work is to show that black-box monitoring of HyperLTL (a logic for hyperproperties) is in general unfeasible, and to suggest a gray-box approach in which we combine static and runtime verification. The main idea is to call a static verifier as an oracle at run time allowing, in some cases, to give a final verdict for properties that are considered to be non-monitorable under a black-box approach. Our third contribution is the instantiation of this solution to a privacy property called distributed data minimization which cannot be verified using black-box runtime verification. We use an SMT-based static verifier as an oracle at run time. We have implemented our gray-box approach for monitoring data minimization into the proof-of-concept tool Minion. We describe the tool and apply it to a few case studies to show its feasibility.
Styles APA, Harvard, Vancouver, ISO, etc.

Thèses sur le sujet "Hyperproperties verification"

1

Pasqua, Michele. « Hyper Static Analysis of Programs - An Abstract Interpretation-Based Framework for Hyperproperties Verification ». Doctoral thesis, 2019. http://hdl.handle.net/11562/995302.

Texte intégral
Résumé :
In the context of systems security, information flows play a central role. Unhandled information flows potentially leave the door open to very dangerous types of security attacks, such as code injection or sensitive information leakage. Information flows verification is based on a notion of dependency between a system’s objects, which requires specifications expressing relations between different executions of a system. Specifications of this kind, called hyperproperties, go beyond classic trace properties, defined in terms of predicate over single executions. The problem of trace properties verification is well studied, both from a theoretical as well as a practical point of view. Unfortunately, very few works deal with the verification of hyperproperties. Note that hyperproperties are not limited to information flows. Indeed, a lot of other important problems can be modeled through hyperproperties only: processes synchronization, availability requirements, integrity issues, error resistant codes check, just to name a few. The sound verification of hyperproperties is not trivial: it is not easy to adapt classic verification methods, used for trace properties, in order to deal with hyperproperties. The added complexity derives from the fact that hyperproperties are defined over sets of sets of executions, rather than sets of executions, as happens for trace properties. In general, passing to powersets involves many problems, from a computability point of view, and this is the case also for systems verification. In this thesis, it is explored the problem of hyperproperties verification in its theoretical and practical aspects. In particular, the aim is to extend verification methods used for trace properties to the more general case of hyperproperties. The verification is performed exploiting the framework of abstract interpretation, a very general theory for approximating the behavior of discrete dynamic systems. Apart from the general setting, the thesis focuses on sound verification methods, based on static analysis, for computer programs. As a case study – which is also a leading motivation – the verification of information flows specifications has been taken into account, in the form of Non-Interference and Abstract Non-Interference. The second is a weakening of the first, useful in the context where Non-Interference is a too restrictive specification. The results of the thesis have been implemented in a prototype analyzer for (Abstract) Non-Interference which is, to the best of the author’s knowledge, the first attempt to implement a sound verifier for that specification(s), based on abstract interpretation and taking into account the expressive power of hyperproperties.
Styles APA, Harvard, Vancouver, ISO, etc.

Chapitres de livres sur le sujet "Hyperproperties verification"

1

Finkbeiner, Bernd, Christopher Hahn, Marvin Stenger et Leander Tentrup. « Monitoring Hyperproperties ». Dans Runtime Verification, 190–207. Cham : Springer International Publishing, 2017. http://dx.doi.org/10.1007/978-3-319-67531-2_12.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
2

Hahn, Christopher. « Algorithms for Monitoring Hyperproperties ». Dans Runtime Verification, 70–90. Cham : Springer International Publishing, 2019. http://dx.doi.org/10.1007/978-3-030-32079-9_5.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
3

Finkbeiner, Bernd, Christopher Hahn et Hazem Torfah. « Model Checking Quantitative Hyperproperties ». Dans Computer Aided Verification, 144–63. Cham : Springer International Publishing, 2018. http://dx.doi.org/10.1007/978-3-319-96145-3_8.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
4

Finkbeiner, Bernd, Christopher Hahn, Jana Hofmann et Leander Tentrup. « Realizing $$\omega $$-regular Hyperproperties ». Dans Computer Aided Verification, 40–63. Cham : Springer International Publishing, 2020. http://dx.doi.org/10.1007/978-3-030-53291-8_4.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
5

Finkbeiner, Bernd, Christopher Hahn, Philip Lukert, Marvin Stenger et Leander Tentrup. « Synthesizing Reactive Systems from Hyperproperties ». Dans Computer Aided Verification, 289–306. Cham : Springer International Publishing, 2018. http://dx.doi.org/10.1007/978-3-319-96145-3_16.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
6

Beutner, Raven, et Bernd Finkbeiner. « Software Verification of Hyperproperties Beyond k-Safety ». Dans Computer Aided Verification, 341–62. Cham : Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-031-13185-1_17.

Texte intégral
Résumé :
AbstractTemporal hyperproperties are system properties that relate multiple execution traces. For (finite-state) hardware, temporal hyperproperties are supported by model checking algorithms, and tools for general temporal logics like HyperLTL exist. For (infinite-state) software, the analysis of temporal hyperproperties has, so far, been limited to k-safety properties, i.e., properties that stipulate the absence of a bad interaction between any k traces. In this paper, we present an automated method for the verification of $$\forall ^k\exists ^l$$ ∀ k ∃ l -safety properties in infinite-state systems. A $$\forall ^k\exists ^l$$ ∀ k ∃ l -safety property stipulates that for any k traces, there existl traces such that the resulting $$k+l$$ k + l traces do not interact badly. This combination of universal and existential quantification enables us to express many properties beyond k-safety, including, for example, generalized non-interference or program refinement. Our method is based on a strategy-based instantiation of existential trace quantification combined with a program reduction, both in the context of a fixed predicate abstraction. Notably, our framework allows for mutual dependence of strategy and reduction.
Styles APA, Harvard, Vancouver, ISO, etc.
7

Baumeister, Jan, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner et César Sánchez. « A Temporal Logic for Asynchronous Hyperproperties ». Dans Computer Aided Verification, 694–717. Cham : Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-81685-8_33.

Texte intégral
Résumé :
AbstractHyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and HyperCTL* have been proposed to express hyperproperties. However, their semantics are synchronous in the sense that all traces proceed at the same speed and are evaluated at the same position. This precludes the use of these logics to analyze systems whose traces can proceed at different speeds and allow that different traces take stuttering steps independently. To solve this problem in this paper, we propose an asynchronous variant of HyperLTL. On the negative side, we show that the model-checking problem for this variant is undecidable. On the positive side, we identify a decidable fragment which covers a rich set of formulas with practical applications. We also propose two model-checking algorithms that reduce our problem to the HyperLTL model-checking problem in the synchronous semantics.
Styles APA, Harvard, Vancouver, ISO, etc.
8

Bonakdarpour, Borzoo, et Bernd Finkbeiner. « Program Repair for Hyperproperties ». Dans Automated Technology for Verification and Analysis, 423–41. Cham : Springer International Publishing, 2019. http://dx.doi.org/10.1007/978-3-030-31784-3_25.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
9

Ábrahám, Erika, Ezio Bartocci, Borzoo Bonakdarpour et Oyendrila Dobe. « Probabilistic Hyperproperties with Nondeterminism ». Dans Automated Technology for Verification and Analysis, 518–34. Cham : Springer International Publishing, 2020. http://dx.doi.org/10.1007/978-3-030-59152-6_29.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
10

Coenen, Norine, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann et Yannick Schillo. « Runtime Enforcement of Hyperproperties ». Dans Automated Technology for Verification and Analysis, 283–99. Cham : Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-88885-5_19.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.

Actes de conférences sur le sujet "Hyperproperties verification"

1

Long, Teng, et Guoqing Yao. « Verification for Security-Relevant Properties and Hyperproperties ». Dans 2015 IEEE 12th Intl. Conf. on Ubiquitous Intelligence and Computing, 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). IEEE, 2015. http://dx.doi.org/10.1109/uic-atc-scalcom-cbdcom-iop.2015.101.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
2

Pinisetty, Srinivas, Gerardo Schneider et David Sands. « Runtime verification of hyperproperties for deterministic programs ». Dans ICSE '18 : 40th International Conference on Software Engineering. New York, NY, USA : ACM, 2018. http://dx.doi.org/10.1145/3193992.3193995.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
3

Anand, Mahathi, Vishnu Murali, Ashutosh Trivedi et Majid Zamani. « Formal verification of hyperproperties for control systems ». Dans CPS-IoT Week '21 : Cyber-Physical Systems and Internet of Things Week 2021. New York, NY, USA : ACM, 2021. http://dx.doi.org/10.1145/3457335.3461715.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
4

Agrawal, Shreya, et Borzoo Bonakdarpour. « Runtime Verification of k-Safety Hyperproperties in HyperLTL ». Dans 2016 IEEE 29th Computer Security Foundations Symposium (CSF). IEEE, 2016. http://dx.doi.org/10.1109/csf.2016.24.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
Nous offrons des réductions sur tous les plans premium pour les auteurs dont les œuvres sont incluses dans des sélections littéraires thématiques. Contactez-nous pour obtenir un code promo unique!

Vers la bibliographie