[Ufmrg] Formal Proofs, the Fine Print and Side Effects
Gergely Buday <g.buday@sheffield.ac.uk> Thu, 01 February 2024 17:04 UTC
Return-Path: <g.buday@sheffield.ac.uk>
X-Original-To: ufmrg@ietfa.amsl.com
Delivered-To: ufmrg@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id D4212C14F5E6 for <ufmrg@ietfa.amsl.com>; Thu, 1 Feb 2024 09:04:30 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -0.706
X-Spam-Level:
X-Spam-Status: No, score=-0.706 tagged_above=-999 required=5 tests=[BAYES_05=-0.5, DKIMWL_WL_MED=-0.001, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, HTML_MESSAGE=0.001, RCVD_IN_ZEN_BLOCKED_OPENDNS=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01, URIBL_BLOCKED=0.001, URIBL_DBL_BLOCKED_OPENDNS=0.001, URIBL_ZEN_BLOCKED_OPENDNS=0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (2048-bit key) header.d=sheffield.ac.uk
Received: from mail.ietf.org ([50.223.129.194]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id mKl6MhOvYFiH for <ufmrg@ietfa.amsl.com>; Thu, 1 Feb 2024 09:04:25 -0800 (PST)
Received: from mail-ej1-x633.google.com (mail-ej1-x633.google.com [IPv6:2a00:1450:4864:20::633]) (using TLSv1.3 with cipher TLS_AES_128_GCM_SHA256 (128/128 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 639BEC14F6F6 for <Ufmrg@irtf.org>; Thu, 1 Feb 2024 09:01:19 -0800 (PST)
Received: by mail-ej1-x633.google.com with SMTP id a640c23a62f3a-a28a6cef709so165239866b.1 for <Ufmrg@irtf.org>; Thu, 01 Feb 2024 09:01:19 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sheffield.ac.uk; s=170424.google; t=1706806877; x=1707411677; darn=irtf.org; h=to:subject:message-id:date:from:mime-version:from:to:cc:subject :date:message-id:reply-to; bh=BARTfYk2KZie7zZGKy2fGSExw4eSJzqZ5k/aSnn4xJM=; b=IRwNPO5PnbLb4VI8Ai+Uber5segj3oC87YrVRx0R4eWpl/jZkQ2vj/kZEhS4fLzYqm 2itFoKxAYRN0Z/Av+lvMoJ1rS4+H5v6wAp2bCI14/zZ//2t+nMpwRXsY7fkgB+QZ2YnX fVq1gthTzAQdgBzFIeqi76VrSVaKBdJ9Bi9GaKa1LAP/aVH96Nn6/wsIw9e7fYl+/sGi 8TLnIwbrinAyeKJevLdOpzSw6/KY1sPuBvdFgH1BtZrlf7/xAt8yWz7ag0YBcS7MpLuv f50IRlXUjOGVspFjljof/jDJb5JJXyBe/EL2wLazjh3lTAcLY1VCydiVrHD23gN1ihRO 2Ubg==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1706806877; x=1707411677; h=to:subject:message-id:date:from:mime-version:x-gm-message-state :from:to:cc:subject:date:message-id:reply-to; bh=BARTfYk2KZie7zZGKy2fGSExw4eSJzqZ5k/aSnn4xJM=; b=B0k2v9s7KwjW516llxqMw/gBIhfZEjVl02+BGresxdO7J9kO6hY4pof0uGDfztbkO0 UnBcg1Ai/W05R+hmmufkOdHLAWLZG3uC7hg7GnevHAApBfxC2lQ/6FpzgIQSaq6u5eLZ 3FhaVy+Dbl5r+pi6jc/VRFP32SDFu56+8bARccBPGQSmNG/bLgUXOb3eVUIEporgmz88 G9nF1PJMsuepgXYpF8ZB0vkTaQXybdFghzWUiGHL/rcj5ZEhZN0P+B3jODRAdrIPF1Zc cXlQiD2cx87Zc3cAzbbgEdZltaYrT8ouuIkxYyQ0HKAH6P+/Oc71zKfA6sfBP5bd5W0I yY8g==
X-Gm-Message-State: AOJu0Yxowy72PDXp8PiTBRwa7n6M316zfalePc/AbM6Tur+bxNOjcKqs f4fQouB/hDzOyyvRTBFTH+xk2Xl/E/YI4th6IxIqgiJCpuzg656GU6N0NI/VRBgjD4uWHQ5AYLo 2NDEqqYRvsPSAvK+U05U7MaDVe3zO5ruqzvNEJd2jLVvbkVnztLIAzA2HD818zQcC5UDUkXR+K+ jvFkk3B5TvcNi9Rpnhzpf8lhgX3Yg3S0zkMD28HVZH80OVt4G0tRCDBBJpHHbzf7kgKWo4zHFn8 17p6zkGtTjBIoGBUkfh
X-Google-Smtp-Source: AGHT+IHkfjXLGaqpUPuSP6PVAFH7vTX8yc1UM2IS2tEeH/9vnGVg4Y0ShXITq9jODHrKXz512iRypIFhY7xOhifov/s=
X-Received: by 2002:a17:906:dfcb:b0:a35:e524:c9a1 with SMTP id jt11-20020a170906dfcb00b00a35e524c9a1mr3687925ejc.14.1706806876886; Thu, 01 Feb 2024 09:01:16 -0800 (PST)
MIME-Version: 1.0
From: Gergely Buday <g.buday@sheffield.ac.uk>
Date: Thu, 01 Feb 2024 17:01:06 +0000
Message-ID: <CAHgAKgQqJ21rvc7orusL57kZizJnn5a6ONLgOY02nCdinA_c=w@mail.gmail.com>
To: Ufmrg@irtf.org
Content-Type: multipart/alternative; boundary="000000000000994cb0061054f1ed"
Archived-At: <https://mailarchive.ietf.org/arch/msg/ufmrg/_-HKKl59R6zxFuxMV1bpk-dwp04>
Subject: [Ufmrg] Formal Proofs, the Fine Print and Side Effects
X-BeenThere: ufmrg@irtf.org
X-Mailman-Version: 2.1.39
Precedence: list
List-Id: Usable Formal Methods Research Group <ufmrg.irtf.org>
List-Unsubscribe: <https://mailman.irtf.org/mailman/options/ufmrg>, <mailto:ufmrg-request@irtf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/ufmrg/>
List-Post: <mailto:ufmrg@irtf.org>
List-Help: <mailto:ufmrg-request@irtf.org?subject=help>
List-Subscribe: <https://mailman.irtf.org/mailman/listinfo/ufmrg>, <mailto:ufmrg-request@irtf.org?subject=subscribe>
X-List-Received-Date: Thu, 01 Feb 2024 17:04:30 -0000
Dear Members, I've thought you might be interested in a paper that thinks about the value of formal proofs applied to real systems. It is a nice read and does not contain too many technicalities, it is more on the philosophical side: https://people.scs.carleton.ca/~paulv/papers/secdev2018.pdf The main takeaway for me is that a formal proof is about a formal model of the system, and we cannot be sure that all our assumptions hold in reality. And then what can we think about the value of our formal proof? The paper has answers. Yours - Gergely
- [Ufmrg] Formal Proofs, the Fine Print and Side Ef… Gergely Buday
- Re: [Ufmrg] Formal Proofs, the Fine Print and Sid… Marc Petit-Huguenin