Готові списки джерел за темами / Hyperproperties verification

Зміст

  1. Статті в журналах
  2. Дисертації
  3. Частини книг
  4. Тези доповідей конференцій

Добірка наукової літератури з теми "Hyperproperties verification"

Автор: Grafiati
Опубліковано: 11 березня 2023

Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями

Оберіть тип джерела:

Ознайомтеся зі списками актуальних статей, книг, дисертацій, тез та інших наукових джерел на тему "Hyperproperties verification".

Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.

Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.

Статті в журналах з теми "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 (October 19, 2019): 1–23. http://dx.doi.org/10.1145/3358232.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
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 (February 20, 2020): 729–40. http://dx.doi.org/10.1007/s10009-020-00552-5.

Повний текст джерела
Анотація:
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.
Стилі APA, Harvard, Vancouver, ISO та ін.
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.

Повний текст джерела
Анотація:
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.
Стилі APA, Harvard, Vancouver, ISO та ін.

Дисертації з теми "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.

Повний текст джерела
Анотація:
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.
Стилі APA, Harvard, Vancouver, ISO та ін.

Частини книг з теми "Hyperproperties verification"

1

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

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
2

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

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
3

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

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
4

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

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
5

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

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
6

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

Повний текст джерела
Анотація:
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.
Стилі APA, Harvard, Vancouver, ISO та ін.
7

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

Повний текст джерела
Анотація:
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.
Стилі APA, Harvard, Vancouver, ISO та ін.
8

Bonakdarpour, Borzoo, and Bernd Finkbeiner. "Program Repair for Hyperproperties." In 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.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
9

Ábrahám, Erika, Ezio Bartocci, Borzoo Bonakdarpour, and Oyendrila Dobe. "Probabilistic Hyperproperties with Nondeterminism." In 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.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
10

Coenen, Norine, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, and Yannick Schillo. "Runtime Enforcement of Hyperproperties." In 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.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.

Тези доповідей конференцій з теми "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.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
2

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

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
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. New York, NY, USA: ACM, 2021. http://dx.doi.org/10.1145/3457335.3461715.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
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.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
Ми пропонуємо знижки на всі преміум-плани для авторів, чиї праці увійшли до тематичних добірок літератури. Зв'яжіться з нами, щоб отримати унікальний промокод!

До бібліографії