Components that should be Open Proofs

From Openproofs

Here are some examples of components which would be great candidates for being open proofs, along with pointers to existing software that might serve as a starting point for an open source software implementation:

• All components in widely-used (enterprise) security application program interfaces (APIs). In particular, everything in the OWASP Enterprise Security API (ESAPI).
• Authentication services, e.g.:
  • PAM - Authentication modules of Unix/Linux Pluggable Authentication Modules (PAM); these are used for local authentication. Start with simple password authentication - pam_unix.
  • LDAP authentication
  • SOAP/WSDL authentication
  • REST authentication. There's some contention on the "right" way to do this. Some info sources: [1] [2] [3] [4] [5]
• Identity Management (related to above).
• Web server
  • See specifications and proved properties by Paul Black in Axiomatic Semantics Verification of a Secure Web Server. Black is willing to release the proofs as OSS. The proofs are of a web server, thttpd, by Fred Cohen. Note that thttpd is not open source software, unfortunately (Wheeler has made requests), so a different implementation would need to be proved to have an open proof.
  • There are already some widely-known FLOSS webservers, including Apache and lighttpd
  • Tornado powers Friendfeed (Apache license) Tornado: Facebook's Real-Time Web Framework for Python (LWN has a review of Tornado)
  • teepeedee2 (fast web server written in Common Lisp for dynamic applications) (LGPL license) - teepeedee2 source code teepeedee2 presentation
  • An implementation should avoid being vulnerable to a slow loris attack - this is a denial-of-service attack, which is often hard to formally specify, but some implementations handle them better than others (lighttpd does well; Apache, not so well)
  • Including correct invocation/limiting of other service via CGI, FastCGI, etc.
• EMail server - JMU did some unpublished efforts with Z and SPARK, funding by State of Virginia. Perhaps releasable.
• Firewall (e.g., the key rule-processing code)
• Network packet sniffer used to detect "malicious" and "unexpected" packets (at its heart this is like the firewall case)
• Remote system-logging service (e.g., syslogd - both client and server side)
• Email signature verification
• Zip file encryption, decryption, and/or signature verification (not the encryption algorithm itself, but its use)
• LISP (Scheme) implementation - see MITRE/Rome Labs VLISP. Many publications, implementation and details unpublished.
• Java Virtual Machine (JVM) implementation. ACL2 folks have done some related work.
• PHP implementation, including interaction with webserver. Issue: Is there an adequate specification?
• Anything setuid root?
• Web clients (eek for size!). Perhaps start with a text client like "links" (Note: lynx may not be maintained anymore)
• Text-based email client (pine? Though not OSS)
• Javascript implementation (Note: Varying implementations). Note: Currently these are undergoing massive changes to increase speed, so any proof will be of very obsolete code
• Operating system kernel, at least parts. Parts: Network stack, filesystem, key drivers (e.g., disk), module system ("system behaves if modules behave"), locking okay
  • Can pick small kernel. See L4-related projects such as the Secure Microkernel Project (seL4) (here's a brief seL4 article) (note that as of 2009-08-13, seL4 is proprietary and not open source software), EROS. ADunn: Note that I think that there's some hope for reasonable licensing for seL4 - a modification of a previous version of L4 - OKL4 - is under dual licensing (BSD-like with restriction that all source code for using projects must be redistributed in the non-commercial version). See http://wiki.ok-labs.com/.
  • TinyOS is an open-source operating system designed for wireless embedded sensor networks. It features a component-based architecture. The paper "High Confidence TinyOS" by John Regehr and Phil Levis argues that TinyOS would make a good starting point for high confidence software.
  • Linux kernel - well-documented (inc. teaching literature), widely-used. There have been some successful model-checking work on the Linux kernel.
  • *BSD kernels - note, MacOS use
  • Funk (GPLv2+) is a small kernel written in OCaml
  • Minix 3 (BSD license) is focused on reliability
• Secure Hypervisor. See NRL Xen work
• "Secure filesystem" - "E.G., No information revealed". There's some Haskell work in this area.
• Crypto libraries: "Always encrypts", etc., presuming the encryption algorithm correct.
  • OpenSSH, OpenSSL. Note existing FIPS certifications.
• Long-term: Prove FM tools themselves (at least their verifiers). See ACL2, prover9. This becomes valuable only if the FM tools themselves are used to prove programs/models.
• Version control software, even against attack (so can verify who did what). See the paper Software Configuration Management (SCM) Security
  • (E.G., import functions of a distributed CM system like git or mercurial)
• Database Management Systems (DBMS). There's lots of work in this area, but note that DBMSs tend to be very large.
• Low-level library (e.g., C library) functions. See ACL2's proofs of C string operations.
• Voting software. See David MENTRE's toy voting program with Frama-C (GPL license), which might be a useful start
• Computer hardware. Perhaps SPARC or ACL2 proofs?

Where possible, see if someone has already specified what it "should" do (RFCs, etc.)

Beyond correctness, can also prove "quality" factors (speed, amount of caching, ability to not crash, resistance to DoS attacks, etc.)