Formalization and verification of a mail server in Coq

AFFELDT, Reynald ; KOBAYASHI, Naoki

In: ISSS 2002 : software security - theories and systems (Tokyo, 8-10 November 2002, revised papers)Lecture notes in computer science; (2003) S. 217-233

Konferenz - print, 15 ref

Wie komme ich dran?

This paper reports on the formalization and verification of a mail server (SMTP server) in Coq. The correctness of a mail server is very important: bugs of the mail server may be abused for eavesdropping mail contents, spreading virus, sending spam messages, etc. We have verified a part of a mail server written in Java, by manually translating the Java program into a Coq function as faithfully as possible, and verifying properties of the Coq function. The results of this experiment indicate the feasibility and usefulness of verification of middle-sized system softwares in this style. The verification has been carried out in a few months, and a few bugs in the mail server have been indeed found during the verification process.

Titel:	Formalization and verification of a mail server in Coq
Autor/in / Beteiligte Person:	AFFELDT, Reynald ; KOBAYASHI, Naoki
Link:	E-Journal im Bestand der UB Hagen? View record from PASCAL Archive
Quelle:	ISSS 2002 : software security - theories and systems (Tokyo, 8-10 November 2002, revised papers)Lecture notes in computer science; (2003) S. 217-233
Veröffentlichung:	Berlin: Springer, 2003
Medientyp:	Konferenz
Umfang:	print, 15 ref
ISSN:	0302-9743 (print)
Schlagwort:	Computer science Informatique Sciences exactes et technologie Exact sciences and technology Sciences appliquees Applied sciences Informatique; automatique theorique; systemes Computer science; control theory; systems Logiciel Software Organisation des mémoires. Traitement des données Memory organisation. Data processing Gestion des mémoires et des fichiers (y compris la protection et la sécurité des fichiers) Memory and file management (including protection and security) Courrier électronique Electronic mail Correo electrónico Démonstration théorème Theorem proving Demostración teorema Langage JAVA JAVA language Lenguaje JAVA Serveur informatique Computer server Servidor informático Sécurité Safety Seguridad Virus informatique Computer virus Virus informático Vérification programme Program verification Verificación programa
Sonstiges:	Nachgewiesen in: PASCAL Archive Sprachen: English Original Material: INIST-CNRS Document Type: Conference Paper File Description: text Language: English Author Affiliations: Department of Computer Science, University of Tokyo, Japan ; Department of Computer Science, Tokyo Institute of Technology, Japan Rights: Copyright 2003 INIST-CNRS ; CC BY 4.0 ; Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS Notes: Computer science; theoretical automation; systems

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.