From c2731fdb4334a289e4e2216a76b75e13263fb73b Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 11 Jun 2021 00:07:55 -0500 Subject: [PATCH] initial --- .gitignore | 1 + CoqSSH.opam | 1 + Extract.v | 6 ++++++ coq_ssh.ml | 37 +++++++++++++++++++++++++++++++++++ crypto_prims.ml | 44 ++++++++++++++++++++++++++++++++++++++++++ dune | 9 +++++++++ dune-project | 2 ++ theories/CryptoPrims.v | 30 ++++++++++++++++++++++++++++ theories/SSH.v | 15 ++++++++++++++ theories/dune | 11 +++++++++++ 10 files changed, 156 insertions(+) create mode 100644 .gitignore create mode 100644 CoqSSH.opam create mode 100644 Extract.v create mode 100644 coq_ssh.ml create mode 100644 crypto_prims.ml create mode 100644 dune create mode 100644 dune-project create mode 100644 theories/CryptoPrims.v create mode 100644 theories/SSH.v create mode 100644 theories/dune diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..9c5f578 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +_build \ No newline at end of file diff --git a/CoqSSH.opam b/CoqSSH.opam new file mode 100644 index 0000000..5538a8b --- /dev/null +++ b/CoqSSH.opam @@ -0,0 +1 @@ +name: "CoqSSH" \ No newline at end of file diff --git a/Extract.v b/Extract.v new file mode 100644 index 0000000..e160ee8 --- /dev/null +++ b/Extract.v @@ -0,0 +1,6 @@ +From Coq Require Extraction. + +Require CSSH. + +Extraction "SSH" SSH. +Extraction "CryptoPrims" CryptoPrims. \ No newline at end of file diff --git a/coq_ssh.ml b/coq_ssh.ml new file mode 100644 index 0000000..03a02b9 --- /dev/null +++ b/coq_ssh.ml @@ -0,0 +1,37 @@ +open Unix +open Printf +open CoqSSH + +let () = + let addr_str = "10.7.0.4" in + + let socket_fd = socket PF_INET SOCK_STREAM 0 in + let inet_addr = inet_addr_of_string addr_str in + let sock_addr = ADDR_INET (inet_addr, 22) in + + connect socket_fd sock_addr; + printf "Connected to %s.\n" addr_str; + + (* protocol negotiation *) + + let hello = "2.0 Hellosu\r\n" |> Bytes.of_string in + let bytes_written = write socket_fd hello 0 (Bytes.length hello) in + printf "Sent greeting (%d bytes).\n" bytes_written; + + let buf = Bytes.create 1024 in + let bytes_read = read socket_fd buf 0 1024 in + let actual = Bytes.sub buf 0 bytes_read |> Bytes.to_string in + printf "Read '%s' (%d bytes).\n" actual bytes_read; + + let version = "SSH-2.0-CoqSSH0.1 Coggers\r\n" |> Bytes.of_string in + let bytes_written = write socket_fd version 0 (Bytes.length version) in + printf "Sent protocol version (%d bytes).\n" bytes_written; + + (* key exchange *) + + let n : SSH.nat = SSH.O in + match n with + | SSH.O -> print_endline "o" + | _ -> (); + + close socket_fd; diff --git a/crypto_prims.ml b/crypto_prims.ml new file mode 100644 index 0000000..3d638ed --- /dev/null +++ b/crypto_prims.ml @@ -0,0 +1,44 @@ +module IFC = struct + (* + "Principals" are people (or hosts, or organizations) that may have + different access to information. It's described here by a string; + each principal has a unique string. + *) + type principal = string + + (* + Labels represent who is allowed to have access to a certain piece + of information. Labels form a lattice, with Public at the bottom and + Secret at the top. + + Every time information flows through the program, + it must be checked to make sure that it's not revealing information + when it isn't allowed to. + + For example, + *) + type label = + (* a list of principals that have access to the information described + by this label *) + | LCanRead of principal list + + (* join of 2 labels *) + | LJoin of label * label + + (* bottom of the lattice *) + | LPublic + + (* base type of bytes *) + type bytes = + (* a literal string *) + | BLit of string + (* 2 sets of byte-strings concatenated *) + | BConcat of bytes * bytes + (* cryptographically random set of bytes *) + | BRand of principal +end + +module type CryptoPrims = sig + (* A function for generating a random nonce of n bytes *) + (* val rand : *) +end \ No newline at end of file diff --git a/dune b/dune new file mode 100644 index 0000000..66d2511 --- /dev/null +++ b/dune @@ -0,0 +1,9 @@ +(executable + (name coq_ssh) + (public_name coq_ssh) + (libraries unix CoqSSH) + (package CoqSSH)) + +(env + (dev + (flags (:standard -warn-error -A)))) diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..c8d78ef --- /dev/null +++ b/dune-project @@ -0,0 +1,2 @@ +(lang dune 2.8) +(using coq 0.3) diff --git a/theories/CryptoPrims.v b/theories/CryptoPrims.v new file mode 100644 index 0000000..e79832e --- /dev/null +++ b/theories/CryptoPrims.v @@ -0,0 +1,30 @@ +From Coq Require Extraction. +Require Import Strings.String. + +(* +Abstract cryptographic primitives. + +For proof-checking, this will resolve to a set of axioms, but when +extracting to ocaml, this should be replaced with the real implementation +of the cryptographic primitives. +*) +Module Type AbsCryptoPrims. + Definition principal : Type := string. + + Inductive label : Set := + Public : label + . +End AbsCryptoPrims. + +Module NullCryptoPrims : AbsCryptoPrims. + Definition principal : Type := string. + + Inductive label : Set := + Public : label + . +End NullCryptoPrims. + +Extraction Language OCaml. +Set Extraction Optimize. +Set Extraction AccessOpaque. +Extraction "CryptoPrims" NullCryptoPrims. diff --git a/theories/SSH.v b/theories/SSH.v new file mode 100644 index 0000000..b473174 --- /dev/null +++ b/theories/SSH.v @@ -0,0 +1,15 @@ +From Coq Require Extraction. +Module SSH. + +Inductive natlist : Type := + | nil + | cons (n : nat) (l : natlist). + +Fixpoint length (l:natlist) : nat := + match l with + | nil => O + | cons h t => S (length t) + end. + +End SSH. +Extraction "SSH" SSH. diff --git a/theories/dune b/theories/dune new file mode 100644 index 0000000..865ea5b --- /dev/null +++ b/theories/dune @@ -0,0 +1,11 @@ +(library + (name CoqSSH) + (package CoqSSH)) + +(coq.extraction + (prelude SSH) + (extracted_modules SSH)) + +(coq.extraction + (prelude CryptoPrims) + (extracted_modules CryptoPrims))