Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
shakedown.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
A community for live music fans with roots in the jam scene. Shakedown Social is run by a team of volunteers (led by @clifff and @sethadam1) and funded by donations.

Administered by:

Server stats:

292
active users

shakedown.social: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.4

#formalverification

0 posts0 participants0 posts today
Rob Sison<p>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:</p><p><a href="https://youtu.be/7wcFx6OTEL4" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/7wcFx6OTEL4</span><span class="invisible"></span></a></p><p><a href="https://aus.social/tags/sel4summit" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>sel4summit</span></a> <a href="https://aus.social/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a> <a href="https://aus.social/tags/verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>verification</span></a> <a href="https://aus.social/tags/operatingsystems" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>operatingsystems</span></a> <a href="https://aus.social/tags/microkernel" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>microkernel</span></a> <a href="https://aus.social/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://aus.social/tags/HOL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HOL4</span></a> <a href="https://aus.social/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://aus.social/tags/modelchecking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>modelchecking</span></a> <a href="https://aus.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://aus.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalverification</span></a> <a href="https://aus.social/tags/formal_methods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formal_methods</span></a> <a href="https://aus.social/tags/formal_verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formal_verification</span></a></p>
Frederic Jacobs<p>One of the challenges with the deployment of more automated reasoning is often the tooling. Cool to see <a href="https://mastodon.social/tags/Cryspen" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Cryspen</span></a> invest in a new integrated development and verification environment based on hax. Congrats <span class="h-card" translate="no"><a href="https://mastodon.social/@franziskus" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>franziskus</span></a></span> and team :) <br><a href="https://cryspen.com/post/cyber-campus-hax/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">cryspen.com/post/cyber-campus-</span><span class="invisible">hax/</span></a></p><p><a href="https://mastodon.social/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalMethods</span></a> <a href="https://mastodon.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a></p>
Frederic Jacobs<p>Galois applied GPT-4 to generate a SAW memory safety proof for salsa20. Interesting example of what's currently possible at the intersection of LLMs and Formal Verification. Clearly more to come in that space.<br><a href="https://mastodon.social/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalMethods</span></a> <a href="https://mastodon.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://mastodon.social/tags/LLM" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLM</span></a> <br><a href="https://galois.com/blog/2023/08/applying-gpt-4-to-saw-formal-verification/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">galois.com/blog/2023/08/applyi</span><span class="invisible">ng-gpt-4-to-saw-formal-verification/</span></a></p>
Frederic Jacobs<p>Gluing together Hacspec, Jasmin and SSProve using Coq for end-to-end verification, from spec to implementation.</p><p>It's great to see more integration efforts between formal verification stacks to improve confidence that implementations still satisfy all higher-level security properties.</p><p><a href="https://mastodon.social/tags/FV" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FV</span></a> <a href="https://mastodon.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a><br><a href="https://eprint.iacr.org/2023/185" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">https://</span><span class="">eprint.iacr.org/2023/185</span><span class="invisible"></span></a></p>
Steve Easterbrook<p>A fuller <a href="https://fediscience.org/tags/introduction" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>introduction</span></a>.</p><p>My PhD was in software systems analysis: how to handle poorly understood, conflicting system requirements (<a href="https://fediscience.org/tags/RequirementsEngineering" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>RequirementsEngineering</span></a>)</p><p>This led me to explore socio-cognitive processes of large teams (<a href="https://fediscience.org/tags/DistributedCognition" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DistributedCognition</span></a>, <a href="https://fediscience.org/tags/STS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>STS</span></a>, <a href="https://fediscience.org/tags/Ethnography" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Ethnography</span></a>)</p><p>I have worked for NASA studying software safety for spacecraft (<a href="https://fediscience.org/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a>, <a href="https://fediscience.org/tags/OrganizationalBehaviour" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>OrganizationalBehaviour</span></a>)</p><p>Now I study <a href="https://fediscience.org/tags/ClimateModels" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ClimateModels</span></a> + do <a href="https://fediscience.org/tags/ClimateData" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ClimateData</span></a> analytics, using all the above, plus <a href="https://fediscience.org/tags/SystemsThinking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SystemsThinking</span></a>, <a href="https://fediscience.org/tags/DataScience" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DataScience</span></a>, &amp; <a href="https://fediscience.org/tags/ML" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ML</span></a></p>
theruran 💻 🌐 :cereal_killer:<p>worth posting this again, for those programmers who are having wicked thoughts of writing security-critical software in C or C++</p><p>Source: "Exploitation in the era of <a href="https://hackers.town/tags/formalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalVerification</span></a>: A peek at a new frontier with <a href="https://hackers.town/tags/Ada" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Ada</span></a> / <a href="https://hackers.town/tags/SPARK" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SPARK</span></a>" by Adam Zabrocki and Alex Tereshkin, <a href="https://hackers.town/tags/DEFCON30" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DEFCON30</span></a>, 2022</p><p><a href="https://hackers.town/tags/infosec" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>infosec</span></a> <a href="https://hackers.town/tags/DEFCON" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DEFCON</span></a></p>
ExploreLive feeds
About