The Coq mailing list

[Jim Fehrle <jfehrle AT sbcglobal.net>]

I would agree with Abhishek.  I would add that if the GUI is running in a web browser, the browser should be treated as insecure.  Most browsers have debuggers that allow examination of local data.  Also some browsers are open source--they could easily be modified by a hacker to do anything.  If your app needs to be secure, the server should always validate requests coming from the client.

---

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Sent: Tuesday, October 10, 2017 1:37 PM
Subject: Re: [Coq-Club] Verification of GUIs in Coq

I am curious what you want to prove about GUIs. 

In the healthcare domain, I guess privacy is the biggest concern. 

I think that a pragmatic approach is to push these concerns to the backend, whose semantics seem much easier to define than the frontends (GUIs) that interact with humans who are too complex creatures to formally reason about.

For example, it may be possible to just argue that the backend, when communicating with the frontend, never reveals sensitive information. Thus, the frontend, in whatever ways it renders the graphics, cannot reveal sensitive information.

I guess the following work is an example:

http://goto.ucsd.edu/quark/

-- Abhishek

http://www.cs.cornell.edu/~aa7 55/

On Mon, Oct 9, 2017 at 8:30 PM, stvienna wiener <stvienna AT gmail.com> wrote:

Hello everyone,


We are verifying GUI applications from the healthcare domain (e.g.,
healthcare processes) in Agda. Is there any related work in Coq? My
searches mostly return papers on how to write GUI front-ends to
theorem provers/Coq but not how to verify GUIs.


Thanks & best regards,
Stephan