RESUME

Jeffrey Valjean Cook

Note: Until recently, this web page had not been updated since 2001. Since then, I took a position as Director of Internal Research and Development at Network Associates Laboratories, and I subsequently retired from this position in February of 2003. My career as a corporate computer scientist is now over, and I am now self-employed.

Previous Disclaimer: the publication of this resume does not imply that I am searching for a job. Quite the contrary, I have an interesting and challenging position (Manager of Internal Research and Development) at NAI Labs, the Security Research Division of Network Associates, Inc., doing work I enjoy. However, I am a firm believer in keeping things up-to-date, just in case, so here we go.

Education

1977: B.S. in Electrical Engineering, Rice University (cum laude, Tau Beta Pi)

1981: M.S. in Computer Science (major in Programming Languages), UCLA

Computer Skills

Operating Systems: Unix (Sun OS, Linux), DOS, Windows 3.1, Windows 95/98/NT

Hardware platforms: Suns, PCs, Lisp Machines

Programming Languages: Java, C, C++, Lisp, various ancient languages (e.g., Fortran, APL, PL/1, Cobol, Pascal, BCPL, Euclid, etc.), plus some assembler and machine languages

Scripting Languages: Perl, Tcl/Tk, Expect, HTML, Unix shell, DOS Shell

Word Processing: Scribe, LaTeX; Microsoft Word, Excel, and PowerPoint

Work Experience

August 1977 - June 1978: Teaching Assistant, UCLA

Taught three quarters of the introductory course in computer science.

July 1978 - September 1981 Graduate Research Assistant, Information Sciences Institute

Worked on the attribute grammar analysis problem for my UCLA master's thesis. Translated the Nelson-Oppen Simplifier from MacLisp to Interlisp. Started developing new decision procedures for the Simplifier.

October 1981 - September 1991: Member of the Technical Staff, The Aerospace Corporation

(1981-1984) Developed decision procedures for the Simplifier, for bitstrings, coverings (set union), arrays, queues, and associative/commutative multiplication. Added new feature sets to the Simplifier. Started work as a system developer for the State Delta Verification System (SDVS), which I ported to Interlisp-VAX, and improved system capabilities and performance.

(1985-1986) Headed the C/30 Microcode Verification Project, which led to the formal, mechanical verification of approximately 1000 lines of microcode for a production computer, the BNN C/30. Wrote a formal description, in ISPS, of the hardware, analyzed the microcode, and developed a proof of microcode correctness. Also did auxiliary SDVS system development.

(1987-1991) Became primary system developer for SDVS. Added Ada verification capabilities to SDVS. Invented and implemented a novel system called DENOTE that employs a semantic metalanguage in which formal denotational semantic specifications may be written, displayed using LaTeX, and executed in Common Lisp.

October 1991 - June 1997: Senior Computer Scientist, Trusted Information Systems

(1992) Did development work on Chaparral (a successor to SDVS) in support of the proof of correctness of code for the Packet Switching Network (PSN). Redesigned and reimplemented a new version of DENOTE called Jeff's Automated Denotational Definition System (JADDS), with improved capabilities and with its subsystems defined recursively using JADDS, and made JADDS available to the public as free software. Started working on a formal denotational semantics for ANSI/ISO standard C. Started working as P.I. on the Truffles project, adding security to an Internet file replication service.

(1993) Designed and implemented a Truffles server machine that hosts Truffles file replication over the Internet and uses a PEM-based e-mail server for negotiating file sharing relationships. Designed and implemented a Trusted Mail Gateway in Perl using the TIS/PEM software. Designed a Trusted Mailing List and a Trusted Mailing List Manager using TIS/PEM. Completed work on the formal denotational semantics for C, which involves a parser and strong type-checker for all of ANSI/ISO standard C, and a denotational semantics for most of C. The formal semantics for C is completely automated, that is, can automatically generate machine-readable denotational semantic definitions of C programs.

(1994) Implemented and tested the Trusted Mailing List and Trusted Mailing List Manager that permits automated, remote management of trusted mailing lists that utilize TIS/PEM for security. Started working as P.I. for the C Object Code Verification Project, whose objective is to automatically prove the correctness of C object code wrt its corresponding source code, using an Nqthm semantics for C developed using the formal denotational semantics of C.

(1995) Designed and implemented a Trusted Software Distributer with associated Trusted Software Certificate Authority for CommerceNet. Integrated support for the FORTEZZA crypto card into the TIS/MOSS software and helped to write an Internet Draft describing the associated MIME interface. Completed work on the Nqthm semantics for a subset of C. Did development work and troubleshooting for the Trusted Mach (TMach) operating system.

(1996) Started working as P.I. for the new incarnation of Truffles called User-Level Truffles (ULT), developed a GUI in TCL/Tk to drive ULT, worked on security policies for ULT, and managed a UCLA grad student and a TIS employee for development work on ULT. Started working on the International Cryptography Experiment (ICE) in the design phase, with the intent of managing development efforts for ICE. Acquired the job of development manager for TIS/MOSS. Wrote specification for a Java API for Public Key Infrastructures and am managing the Java development work for this effort. Becoming interested in issues wrt Java security and the application of formal methods to the improvement thereof.

June 1997 - May 1998 : Principal Computer Scientist, Trusted Information Systems

(1997) My primary focus during 1997 was on the International Cryptography Experiment (ICE), with a secondary focus on a project for touting the benefits of threshold cryptography for data surety in the International Monitoring System for the Comprehensive Nuclear Test Ban Treaty. For ICE, I initiated improvements to an ASN.1 compiler and the development of a certificate management system (CMS) for X.509 certificates. We also designed an implemented a Unix version of Microsoft CryptoAPI 1.0, with support for two Cryptographic Service Providers (CSPs), one for RSA based on RSAREF and another for FORTEZZA. During the latter part of the year, two new projects were initiated, one that involves the implementation of the Public Key Login (PKL) protocol, for both RSA and FORTEZZA, and another that involves implementing an S/MIME plugin for Eudora, based on the Independent Data Unit Protection (IDUP) version of the Generic Security Services (GSS) API.

(1998) I supervised the completion of the PKL project and the S/MIME plugin for Eudora project, and oversaw development of a Cryptographic Service Provider (CSP) for the DSA algorithm, under the Common Data Security Architecture (CDSA) framework.

May 1998 - present : Manager of Internal Research and Development, NAI Labs, the Security Research Division of Network Associates, Inc.

(1998) My job as Manager of IR&D is twofold. First, I manage a team that performs a technology transfer job, that is, transfers research technology to NAI product lines. Examples of such work is the inclusion of X.509 Public Key Infrastucture capabilities into PGP (Pretty Good Privacy), FIPS 140-1 validation for PGP, Gauntlet firewall and VPN performance analysis, and recommendations for Gauntlet firewall performance enhancements. Second, I oversee basic internal research at NAI Labs, research that is crucial to maintaining our cutting edge in order to obtain research grants from the Department of Defense (primarily DARPA) and elsewhere.

References

Available upon request.

Publications

• Barrel Ponds, by Jeff Cook, Koi USA, July/August, 1998, pp 59-61.
• Internet Secure Electronic Mail: Algorithms, Modes, and Identifiers for FORTEZZA Cryptography, by D. Balenson, J. Cook, and R. Housley, Internet Draft, August, 1996.
• Biologically Inspired Topics in Computer Security and Five-Minute Research Talks from the 1996 IEEE Symposium on Security and Privacy, by Jeff Cook, Data Security Letter, Number 72, June, 1996.
• A Java Application Program Interface for Public Key Infrastructures, by Jeffrey V. Cook, Trusted Information Systems, Technical Report 613D, June, 1996.
• Automatic Verification of Object Code Against Source Code, by Sakthi Subramanian and Jeffrey V. Cook. Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS'96), June, 1996.
• Mechanical Verification of C Programs, by Sakthi Subramanian and Jeffrey V. Cook. Proceedings of the ACM SIGSOFT Workshop on Formal Methods in Software Practice, January, 1996.
• A Formal Semantics for C in Nqthm, by Jeffrey V. Cook and Sakthi Subramanian, Trusted Information Systems, Technical Report 517D, October, 1994.
• A Formal Denotational Semantics for C, by Jeffrey V. Cook, Eve Cohen, and Tim Redmond, Trusted Information Systems, Technical Report 409D, September, 1994.
• Trusted Mail Gateways for Confidentiality of Inter-site E-mail, by Jeffrey V. Cook, Trusted Information Systems, Report 541D, July, 1993.
• Truffles: Secure File Sharing With Minimal System Administrator Intervention, by Jeffrey V. Cook, Stephen D. Crocker, Thomas Page, Jr., Gerald Popek, and Peter Reiher, Proceedings of SANS-II, The World Conference On Tools and Techniques For System Administration, Networking, and Security, April, 1993.
• Security Issues in the Truffles File System, by Jeffrey V. Cook, Stephen D. Crocker, Thomas Page, Jr., Gerald Popek, and Peter Reiher, Proceedings of the Privacy and Security Research Group: Workshop on Network and Distributed System Security, February, 1993.
• An Experiment in Using the Hunt/Brock HDL, by Jeffrey V. Cook, Trusted Information Systems, Technical Report 428D, December, 1992.
• An Introduction to Jeff's Automated Denotational Definition System (JADDS), by Jeffrey V. Cook, Trusted Information Systems, Technical Report 402, July, 1992.
• Exponential Complexity of the Covering Solver, by Jeffrey V. Cook, Trusted Information Systems, Technical Report 394, February, 1992.
• Example Proofs of Stage 3 Ada Programs in the State Delta Verification System, by Jeffrey V. Cook, The Aerospace Corporation, ATR-90(6778)-3.
• A Modular Correctness Proof of a Quicksort Procedure Written in Ada using SDVS, by Jeffrey V. Cook and John E. Doner, The Aerospace Corporation, ATR-90(6778)-3.
• A Formal Description of the Incremental Translation of Stage 3 Ada into State Deltas in the State Delta Verification System, by Jeffrey V. Cook, The Aerospace Corporation, ATR-91(6778)-2.
• SDVS Tutorial, co-authored, The Aerospace Corporation, ATR-91(6778)-1.
• Formal Computer Verification in the State Delta Verification System (SDVS), co-authored, AIAA Computers in Aerospace Conference, 1991.
• Offline Characterization of Procedures in the State Delta Verification System, by Jeffrey V. Cook and John E. Doner, The Aerospace Corporation, TR-0090(5920-07)-5.
• Example Proofs using Offline Characterization of Procedures in the State Delta Verification System, by Jeffrey V. Cook and John E. Doner, The Aerospace Corporation, TR-0090(5920-07)-3.
• DENOTE (Denotational Semantics Translation Environment), by Jeffrey V. Cook, The Aerospace Corporation, TR-0090(5920-07)-1.
• The Language for DENOTE, by Jeffrey V. Cook, The Aerospace Corporation, TR-0090(5920-07)-3.
• The Verification of the C/30 Microcode using the State Delta Verification System, by Jeffrey V. Cook, Proceedings of the 13th National Computer Security Conference, 1990.
• User Defined Data Types in the State Delta Verification System, by Jeffrey V. Cook and John E. Doner, The Aerospace Corporation, TR-0090(5920-07)-1.
• Example Proofs of Stage 2 Ada Programs in the State Delta Verification System, by Jeffrey V. Cook, and David F. Martin, The Aerospace Corporation, ATR-90(5778)-1.
• Example Proofs of Stage 1 Ada Programs in the State Delta Verification System, by Jeffrey V. Cook, and John E. Doner, The Aerospace Corporation, ATR-89(4778)-8.
• Test Suite for Static Semantic Errors in ISPS Descriptions, by Jeffrey V. Cook, The Aerospace Corporation, ATR-89(4778)-3.
• Adding Ada Program Verification Capability to the State Delta Verification System, by David F. Martin and Jeffrey V. Cook, Proceedings of the 11th National Computer Security Conference, 1988.
• Example Proofs of Core Ada Programs in the State Delta Verification System, by Timothy A. Aiken, Jeffrey V. Cook, and Leo G. Marcus, The Aerospace Corporation, ATR-88(3778)-3.
• Test Suite for Static Semantic Errors in Core Ada Programs, by Jeffrey V. Cook, The Aerospace Corporation, ATR-88(3778)-3.
• Implementing the Formal Description of the Incremental Translation of Core Ada into State Deltas, by Jeffrey V. Cook, The Aerospace Corporation, ATR-88(3778)-2.
• C/30 Proof, by Jeffrey V. Cook, The Aerospace Corporation, ATR-86(6771)-4.
• Final Report for the C/30 Microcode Verification Project, by Jeffrey V. Cook, The Aerospace Corporation, ATR-86(6771)-3.
• Proof Strategy for the Verification of the C/30 Microcode, by Jeffrey V. Cook, The Aerospace Corporation, ATR-86(6778)-1.
• A Formal Description of the C/30 Virtual Computer, by Jeffrey V. Cook, The Aerospace Corporation, ATR-86(6771)-2.
• A Formal Description of the Microprogrammable Building Block Configured for the C/30 Computer, by Jeffrey V. Cook, Stephen D. Crocker, and M. M. Cutler, The Aerospace Corporation, ATR-86(6771)-1.
• SDVS User Manual, by Leo G. Marcus and Jeffrey V. Cook, The Aerospace Corporation, ATR-84(8478)-1.
• Attribute Grammar Analysis and Processing Experiment (AGAPE), by Jeffrey V. Cook, Master's Thesis, UCLA, 1981.

---

Copyright (C) 1996-2003, Jeffrey Valjean Cook

Maintained by: Jeff Cook (jvcook@comcast.net)
Last updated: 3 October 2003