Bibliografías temáticas / Hyperproperties verification

Índice

  1. Artículos de revistas
  2. Tesis
  3. Capítulos de libros
  4. Actas de conferencias

Literatura académica sobre el tema "Hyperproperties verification"

Autor: Grafiati
Publicado: 11 de marzo de 2023

Crea una cita precisa en los estilos APA, MLA, Chicago, Harvard y otros

Elija tipo de fuente:

Consulte las listas temáticas de artículos, libros, tesis, actas de conferencias y otras fuentes académicas sobre el tema "Hyperproperties verification".

Junto a cada fuente en la lista de referencias hay un botón "Agregar a la bibliografía". Pulsa este botón, y generaremos automáticamente la referencia bibliográfica para la obra elegida en el estilo de cita que necesites: APA, MLA, Harvard, Vancouver, Chicago, etc.

También puede descargar el texto completo de la publicación académica en formato pdf y leer en línea su resumen siempre que esté disponible en los metadatos.

Artículos de revistas sobre el tema "Hyperproperties verification"

1

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

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
2

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

Texto completo
Resumen
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.
Los estilos APA, Harvard, Vancouver, ISO, etc.
3

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

Texto completo
Resumen
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.
Los estilos APA, Harvard, Vancouver, ISO, etc.

Tesis sobre el tema "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.

Texto completo
Resumen
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.
Los estilos APA, Harvard, Vancouver, ISO, etc.

Capítulos de libros sobre el tema "Hyperproperties verification"

1

Finkbeiner, Bernd, Christopher Hahn, Marvin Stenger, and Leander Tentrup. "Monitoring Hyperproperties." In Runtime Verification. Springer International Publishing, 2017. http://dx.doi.org/10.1007/978-3-319-67531-2_12.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
2

Hahn, Christopher. "Algorithms for Monitoring Hyperproperties." In Runtime Verification. Springer International Publishing, 2019. http://dx.doi.org/10.1007/978-3-030-32079-9_5.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
3

Finkbeiner, Bernd, Christopher Hahn, and Hazem Torfah. "Model Checking Quantitative Hyperproperties." In Computer Aided Verification. Springer International Publishing, 2018. http://dx.doi.org/10.1007/978-3-319-96145-3_8.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
4

Finkbeiner, Bernd, Christopher Hahn, Jana Hofmann, and Leander Tentrup. "Realizing $$\omega $$-regular Hyperproperties." In Computer Aided Verification. Springer International Publishing, 2020. http://dx.doi.org/10.1007/978-3-030-53291-8_4.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
5

Finkbeiner, Bernd, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. "Synthesizing Reactive Systems from Hyperproperties." In Computer Aided Verification. Springer International Publishing, 2018. http://dx.doi.org/10.1007/978-3-319-96145-3_16.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
6

Beutner, Raven, and Bernd Finkbeiner. "Software Verification of Hyperproperties Beyond k-Safety." In Computer Aided Verification. Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-031-13185-1_17.

Texto completo
Resumen
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.
Los estilos APA, Harvard, Vancouver, ISO, etc.
7

Baumeister, Jan, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. "A Temporal Logic for Asynchronous Hyperproperties." In Computer Aided Verification. Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-81685-8_33.

Texto completo
Resumen
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.
Los estilos APA, Harvard, Vancouver, ISO, etc.
8

Bonakdarpour, Borzoo, and Bernd Finkbeiner. "Program Repair for Hyperproperties." In Automated Technology for Verification and Analysis. Springer International Publishing, 2019. http://dx.doi.org/10.1007/978-3-030-31784-3_25.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
9

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

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
10

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

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.

Actas de conferencias sobre el tema "Hyperproperties verification"

1

Long, Teng, and Guoqing Yao. "Verification for Security-Relevant Properties and Hyperproperties." In 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.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
2

Pinisetty, Srinivas, Gerardo Schneider, and David Sands. "Runtime verification of hyperproperties for deterministic programs." In ICSE '18: 40th International Conference on Software Engineering. ACM, 2018. http://dx.doi.org/10.1145/3193992.3193995.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
3

Anand, Mahathi, Vishnu Murali, Ashutosh Trivedi, and Majid Zamani. "Formal verification of hyperproperties for control systems." In CPS-IoT Week '21: Cyber-Physical Systems and Internet of Things Week 2021. ACM, 2021. http://dx.doi.org/10.1145/3457335.3461715.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
4

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

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
Ofrecemos descuentos en todos los planes premium para autores cuyas obras están incluidas en selecciones literarias temáticas. ¡Contáctenos para obtener un código promocional único!

Pasar a la bibliografía