Mastodawn

Design and Explore Noise Handshake Patterns (2018)
https://noiseexplorer.com/
#ycombinator #noise_protocol #protocol_verification #formal_verification #noise_protocol_framework #symbolic_verification

Noise Explorer

Noise Explorer is an online engine for reasoning about Noise Protocol Framework Handshake Patterns. Noise Explorer allows you to design and validate Noise Handshake Patterns, to generate cryptographic models for formal verification and to explore a compendium of formal verification results for the most popular and relevant Noise Handshake Patterns in use today.

Habr Dec 10, 2024

Формальная верификация протокола IBFT: проверяем безопасность византийского консенсуса в блокчейне

Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты формальной верификации для предотвращения уязвимостей в различных компонентах блокчейна. Ранее мы верифицировали смарт-контракты дедуктивным методом . В этот раз речь пойдет о протоколах консенсуса — механизмах принятия узлами новых транзакций в цепочку, а именно об алгоритме Istanbul Byzantine Fault Tolerant и в целом о том, как можно гарантировать корректность подобных алгоритмов с помощью метода проверки моделей.

https://habr.com/ru/companies/pt/articles/864754/

#формальная_верификация #formal_verification #протокол_консенсуса #блокчейн #криптовалюты #tla+ #model_checking #IBFT #bft

Формальная верификация протокола IBFT: проверяем безопасность византийского консенсуса в блокчейне

Хабр

Louise Dennis Nov 19, 2024

I have a PDRA post available in Assurance for Robotic Autonomous Systems. Really looking for someone with some experience of formal verification or possibly a background in CyberSecurity. Details at: https://www.jobs.manchester.ac.uk/Job/JobDetail?isPreview=Yes&jobid=30831&advert=external #formal_verification #formal_methods #academic_jobs

Research Associate - Assurance for Robotic Autonomous Systems:Manchester

Show thread

Rob Sison Nov 9, 2024

There's now a video up of the talk I gave at this year's seL4 Summit, on the status of UNSW's projects to verify Time Protection and Microkit-based userland OS services for the seL4 microkernel:

https://youtu.be/7wcFx6OTEL4

#sel4summit #seL4 #verification #operatingsystems #microkernel #IsabelleHOL #HOL4 #ITP #modelchecking #formalmethods #formalverification #formal_methods #formal_verification

Verification Status of Time Protection and Microkit-based OS Services - Rob Sison

YouTube

Louise Dennis May 29, 2024

My AAMAS paper with Mengwei Xu and Mustafa A. Mustafa on Safeguard Privacy for Minimal Data Collection with Trustworthy Autonomous Agents (https://www.ifaamas.org/Proceedings/aamas2024/pdfs/p1966.pdf) is available #OpenAccess. We take the idea that you could have a program that negotiates access to personal data with services on your behalf and ask how you might verify that such a program was behaving correctly. #Privacy #formal_verification #bdi

Alavi | علوی May 5, 2024

Meet #Verus, a tool for formal verification of #Rust programs.
I haven't used it yet, but anything related to formal verification is really interesting to me :D
You guys give it a try and let me know how good it is (it's in very early development)

https://github.com/verus-lang/verus

#formal_methods #formal_verification
#verification

GitHub - verus-lang/verus: Verified Rust for low-level systems code

Verified Rust for low-level systems code. Contribute to verus-lang/verus development by creating an account on GitHub.

GitHub

Habr Apr 3, 2024

Формальная верификация смарт-контрактов во фреймворке ConCert

Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье мы продолжим обсуждать методы и инструменты формальной верификации смарт-контрактов и их практическое применение для предотвращения уязвимостей. Мы подробно поговорим о методе дедуктивной верификации, а точнее, о фреймворке для тестирования и верификации смарт-контрактов — ConCert. Под кат

https://habr.com/ru/companies/pt/articles/804861/

#формальная_верификация #формальная_верификация_криптовалют #formal_verification #formal_methods #тестирование #смартконтракты #блокчейн #solidity #coq #Concert

Формальная верификация смарт-контрактов во фреймворке ConCert

Хабр

nope Feb 12, 2023

Should Computer Programs Be Verified
(1978) : Meyer, Steven
DOI: https://doi.org/10.1145/1010751.1010756
#verification #computer_science #formal_verification #my_bibtex

Should computer programs be verified? | ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes

nope Jan 14, 2023

Slicing Agent Programs for More Efficient Verification
(2019) : Michael Winikoff and Louise Dennis and Michael Fisher
DOI: https://doi.org/10.1007/978-3-030-25693-7_8
#BDI #MAS #bounded_model_checking #formal_verification #gwendolen #model_checking #
#my_bibtex

nope Oct 1, 2022

Tools and Methodologies for Verifying Answer Set Programs
(2022) : Zach Hansen
DOI: https://doi.org/10.48550/ARXIV.2208.03096
#formal_verification #answer_set_programming #ASP #ANTHEM
#my_bibtex

Tools and Methodologies for Verifying Answer Set Programs

Answer Set Programming (ASP) is a powerful declarative programming paradigm commonly used for solving challenging search and optimization problems. The modeling languages of ASP are supported by sophisticated solving algorithms (solvers) that make the solution search efficient while enabling the programmer to model the problem at a high level of abstraction. As an approach to Knowledge Representation and Reasoning, ASP benefits from its simplicity, conciseness and rigorously defined semantics. These characteristics make ASP a straightforward way to develop formally verifiable programs. In the context of artificial intelligence (AI), the clarity of ASP programs lends itself to the construction of explainable, trustworthy AI. In support of these goals, my research is concerned with extending the theory and tools supporting the verification of ASP progams.

arXiv.org