security/libsparkcrypto: Cryptographic library implemented in SPARK

libsparkcrypto is a formally verified implementation of several widely used
symmetric cryptographic algorithms using the SPARK programming language and
toolset. For the complete library proofs of the absence of run-time errors
like type range violations, division by zero and numerical overflows are
available. Some of its subprograms include proofs of partial correctness.

The distribution contains test cases for all implemented algorithms and a
benchmark to compare its performance with the OpenSSL library. The achieved
speed has been found to be very close to the optimized C and Assembler
implementations of OpenSSL.

WWW: http://senier.net/libsparkcrypto/

PR:		ports/180015
Submitted by:	John Marino <draco@marino.st>

7 files changed, 191 insertions, 0 deletions

diff --git a/security/Makefile b/security/Makefile
index 3cf454d2a43b..730aeceb9943 100644
--- a/security/Makefile
+++ b/security/Makefile
@@ -282,6 +282,7 @@
     SUBDIR += libpwstor
     SUBDIR += libsectok
     SUBDIR += libsodium
+    SUBDIR += libsparkcrypto
     SUBDIR += libssh
     SUBDIR += libssh2
     SUBDIR += libtasn1
diff --git a/security/libsparkcrypto/Makefile b/security/libsparkcrypto/Makefile
new file mode 100644
index 000000000000..50742a6e9680
--- /dev/null
+++ b/security/libsparkcrypto/Makefile
@@ -0,0 +1,39 @@
+# Created by: John Marino <draco@marino.st>
+# $FreeBSD$
+
+PORTNAME=	libsparkcrypto
+PORTVERSION=	0.1.1
+CATEGORIES=	security
+MASTER_SITES=	http://senier.net/libsparkcrypto/
+EXTRACT_SUFX=	.tgz
+
+MAINTAINER=	draco@marino.st
+COMMENT=	Cryptographic library implemented in SPARK
+
+LICENSE=	BSD
+
+USES=		ada
+USE_GMAKE=	yes
+USE_DOS2UNIX=	Makefile build/libsparkcrypto.gpr
+SPARKARCH:=	${ARCH:S/amd64/x86_64/:S/i386/i686/}
+
+# The APIDOC requires AdaBrowse which in turn requires ASIS which is
+# coupled with the compiler.  There is a question whether Adacore's
+# GPL ASIS is even compatible with FSF GNAT, which is what gcc-aux is.
+# Until this question is answered, skip API document building.
+
+MAKE_ENV+=	SPARKARCH=${SPARKARCH} \
+		SPARK_DIR=${WRKSRC}/src/spark \
+		DESTDIR=${LOCALBASE} \
+		MODE=release \
+		RUNTIME=native \
+		NO_TESTS=true \
+		NO_PROOF=true \
+		NO_APIDOC=true
+
+post-patch:
+	# ports passed unwanted ARCH definition to Makefile
+	@${REINPLACE_CMD} -e 's|ARCH|SPARKARCH|g' \
+		${WRKSRC}/Makefile
+
+.include <bsd.port.mk>
diff --git a/security/libsparkcrypto/distinfo b/security/libsparkcrypto/distinfo
new file mode 100644
index 000000000000..b32135fb105a
--- /dev/null
+++ b/security/libsparkcrypto/distinfo
@@ -0,0 +1,2 @@
+SHA256 (libsparkcrypto-0.1.1.tgz) = 47582d6910b8c5bb46df51d0e76c27e6fa2b13e8ab73fb4ae0f1d9f7cbd7aa6a
+SIZE (libsparkcrypto-0.1.1.tgz) = 101491
diff --git a/security/libsparkcrypto/files/patch-Makefile b/security/libsparkcrypto/files/patch-Makefile
new file mode 100644
index 000000000000..85ca219ac02b
--- /dev/null
+++ b/security/libsparkcrypto/files/patch-Makefile
@@ -0,0 +1,36 @@
+--- Makefile.orig	2013-06-26 21:03:13.000000000 +0000
++++ Makefile
+@@ -154,21 +154,22 @@ $(OUTPUT_DIR)/proof/libsparkcrypto.idx:
+ install: $(INSTALL_DEPS)
+ 
+ install_files: build
+-	install -d -m 755 $(DESTDIR)/adalib $(DESTDIR)/adainclude $(DESTDIR)/sharedinclude
+-	install -p -m 755 $(OUTPUT_DIR)/build/adalib/libsparkcrypto.a $(DESTDIR)/adalib/libsparkcrypto.a
+-	install -p -m 644 build/libsparkcrypto.gpr $(DESTDIR)/libsparkcrypto.gpr
+-	install -p -m 644 src/shared/$(ENDIANESS)/*.ad? $(DESTDIR)/sharedinclude/
+-	install -p -m 644 src/shared/generic/*.ad? $(DESTDIR)/sharedinclude/
+-	install -p -m 644 src/ada/generic/*.ad? $(DESTDIR)/adainclude/
+-	install -p -m 644 src/ada/$(IO)/*.ad? $(DESTDIR)/adainclude/
++	install -d -m 755 $(DESTDIR)/lib/libsparkcrypto $(DESTDIR)/include/libsparkcrypto/adainclude
++	install -d -m 755 $(DESTDIR)/lib/gnat $(DESTDIR)/include/libsparkcrypto/sharedinclude
++	install -p -m 755 $(OUTPUT_DIR)/build/adalib/libsparkcrypto.a $(DESTDIR)/lib/libsparkcrypto/libsparkcrypto.a
++	install -p -m 644 build/libsparkcrypto.gpr $(DESTDIR)/lib/gnat/libsparkcrypto.gpr
++	install -p -m 644 src/shared/$(ENDIANESS)/*.ad? $(DESTDIR)/include/libsparkcrypto/sharedinclude/
++	install -p -m 644 src/shared/generic/*.ad? $(DESTDIR)/include/libsparkcrypto/sharedinclude/
++	install -p -m 644 src/ada/generic/*.ad? $(DESTDIR)/include/libsparkcrypto/adainclude/
++	install -p -m 644 src/ada/$(IO)/*.ad? $(DESTDIR)/include/libsparkcrypto/adainclude/
+ ifneq ($(strip $(ARCH_FILES)),)
+-	install -p -m 644 $(ARCH_FILES) $(DESTDIR)/adainclude/
++	install -p -m 644 $(ARCH_FILES) $(DESTDIR)/include/libsparkcrypto/adainclude/
+ endif
+-	install -p -m 444 $(OUTPUT_DIR)/build/adalib/*.ali $(DESTDIR)/adalib/
++	install -p -m 444 $(OUTPUT_DIR)/build/adalib/*.ali $(DESTDIR)/lib/libsparkcrypto/
+ 
+ install_proof: install_files proof
+-	install -D -p -m 444 $(OUTPUT_DIR)/proof/libsparkcrypto.sum $(DESTDIR)/libsparkcrypto.sum
+-	(cd $(OUTPUT_DIR)/empty && sparkmake -include=*\.ads -dir=$(DESTDIR)/sharedinclude -nometa -index=$(DESTDIR)/libsparkcrypto.idx)
++	install -D -p -m 444 $(OUTPUT_DIR)/proof/libsparkcrypto.sum $(DESTDIR)/include/libsparkcrypto/libsparkcrypto.sum
++	(cd $(OUTPUT_DIR)/empty && sparkmake -include=*\.ads -dir=$(DESTDIR)/include/libsparkcrypto/sharedinclude -nometa -index=$(DESTDIR)/include/libsparkcrypto/libsparkcrypto.idx)
+ 
+ install_local: DESTDIR = $(OUTPUT_DIR)/libsparkcrypto
+ install_local: install
diff --git a/security/libsparkcrypto/files/patch-build_libsparkcrypto.gpr b/security/libsparkcrypto/files/patch-build_libsparkcrypto.gpr
new file mode 100644
index 000000000000..2483214ff5c5
--- /dev/null
+++ b/security/libsparkcrypto/files/patch-build_libsparkcrypto.gpr
@@ -0,0 +1,13 @@
+--- build/libsparkcrypto.gpr.orig	2013-06-26 21:14:37.000000000 +0000
++++ build/libsparkcrypto.gpr
+@@ -1,7 +1,8 @@
+ project Libsparkcrypto
+ is
+-   for Source_Dirs  use ("adainclude", "sharedinclude");
+-   for Library_Dir  use "adalib";
++   for Source_Dirs  use ("../../include/libsparkcryto/adainclude",
++      "../../include/libsparkcrypto/sharedinclude");
++   for Library_Dir  use "../libsparkcrypto";
+    for Library_Kind use "static";
+    for Library_Name use "sparkcrypto";
+    for Externally_Built use "true";
diff --git a/security/libsparkcrypto/pkg-descr b/security/libsparkcrypto/pkg-descr
new file mode 100644
index 000000000000..cb64120ca02b
--- /dev/null
+++ b/security/libsparkcrypto/pkg-descr
@@ -0,0 +1,12 @@
+libsparkcrypto is a formally verified implementation of several widely used
+symmetric cryptographic algorithms using the SPARK programming language and
+toolset. For the complete library proofs of the absence of run-time errors
+like type range violations, division by zero and numerical overflows are
+available. Some of its subprograms include proofs of partial correctness.
+
+The distribution contains test cases for all implemented algorithms and a
+benchmark to compare its performance with the OpenSSL library. The achieved
+speed has been found to be very close to the optimized C and Assembler
+implementations of OpenSSL.
+
+WWW: http://senier.net/libsparkcrypto/
diff --git a/security/libsparkcrypto/pkg-plist b/security/libsparkcrypto/pkg-plist
new file mode 100644
index 000000000000..dcf247b16788
--- /dev/null
+++ b/security/libsparkcrypto/pkg-plist
@@ -0,0 +1,88 @@
+include/libsparkcrypto/adainclude/lsc-aes-print.adb
+include/libsparkcrypto/adainclude/lsc-aes-print.ads
+include/libsparkcrypto/adainclude/lsc-byteswap32.adb
+include/libsparkcrypto/adainclude/lsc-byteswap64.adb
+include/libsparkcrypto/adainclude/lsc-debug.ads
+include/libsparkcrypto/adainclude/lsc-io.adb
+include/libsparkcrypto/adainclude/lsc-ripemd160-print.adb
+include/libsparkcrypto/adainclude/lsc-ripemd160-print.ads
+include/libsparkcrypto/adainclude/lsc-test.adb
+include/libsparkcrypto/adainclude/lsc-types.adb
+include/libsparkcrypto/sharedinclude/lsc-aes-cbc.adb
+include/libsparkcrypto/sharedinclude/lsc-aes-cbc.ads
+include/libsparkcrypto/sharedinclude/lsc-aes-print.ads
+include/libsparkcrypto/sharedinclude/lsc-aes-tables.ads
+include/libsparkcrypto/sharedinclude/lsc-aes.adb
+include/libsparkcrypto/sharedinclude/lsc-aes.ads
+include/libsparkcrypto/sharedinclude/lsc-byteorder32.adb
+include/libsparkcrypto/sharedinclude/lsc-byteorder32.ads
+include/libsparkcrypto/sharedinclude/lsc-byteorder64.adb
+include/libsparkcrypto/sharedinclude/lsc-byteorder64.ads
+include/libsparkcrypto/sharedinclude/lsc-byteswap32.adb
+include/libsparkcrypto/sharedinclude/lsc-byteswap32.ads
+include/libsparkcrypto/sharedinclude/lsc-byteswap64.adb
+include/libsparkcrypto/sharedinclude/lsc-byteswap64.ads
+include/libsparkcrypto/sharedinclude/lsc-debug.ads
+include/libsparkcrypto/sharedinclude/lsc-hmac_ripemd160.adb
+include/libsparkcrypto/sharedinclude/lsc-hmac_ripemd160.ads
+include/libsparkcrypto/sharedinclude/lsc-hmac_sha256.adb
+include/libsparkcrypto/sharedinclude/lsc-hmac_sha256.ads
+include/libsparkcrypto/sharedinclude/lsc-hmac_sha384.adb
+include/libsparkcrypto/sharedinclude/lsc-hmac_sha384.ads
+include/libsparkcrypto/sharedinclude/lsc-hmac_sha512.adb
+include/libsparkcrypto/sharedinclude/lsc-hmac_sha512.ads
+include/libsparkcrypto/sharedinclude/lsc-io.ads
+include/libsparkcrypto/sharedinclude/lsc-ops32.adb
+include/libsparkcrypto/sharedinclude/lsc-ops32.ads
+include/libsparkcrypto/sharedinclude/lsc-ops64.adb
+include/libsparkcrypto/sharedinclude/lsc-ops64.ads
+include/libsparkcrypto/sharedinclude/lsc-pad32.adb
+include/libsparkcrypto/sharedinclude/lsc-pad32.ads
+include/libsparkcrypto/sharedinclude/lsc-pad64.adb
+include/libsparkcrypto/sharedinclude/lsc-pad64.ads
+include/libsparkcrypto/sharedinclude/lsc-ripemd160-print.ads
+include/libsparkcrypto/sharedinclude/lsc-ripemd160.adb
+include/libsparkcrypto/sharedinclude/lsc-ripemd160.ads
+include/libsparkcrypto/sharedinclude/lsc-sha256-tables.ads
+include/libsparkcrypto/sharedinclude/lsc-sha256.adb
+include/libsparkcrypto/sharedinclude/lsc-sha256.ads
+include/libsparkcrypto/sharedinclude/lsc-sha512-tables.ads
+include/libsparkcrypto/sharedinclude/lsc-sha512.adb
+include/libsparkcrypto/sharedinclude/lsc-sha512.ads
+include/libsparkcrypto/sharedinclude/lsc-test.ads
+include/libsparkcrypto/sharedinclude/lsc-types.ads
+include/libsparkcrypto/sharedinclude/lsc.ads
+lib/gnat/libsparkcrypto.gpr
+lib/libsparkcrypto/libsparkcrypto.a
+lib/libsparkcrypto/lsc-aes-cbc.ali
+lib/libsparkcrypto/lsc-aes-print.ali
+lib/libsparkcrypto/lsc-aes-tables.ali
+lib/libsparkcrypto/lsc-aes.ali
+lib/libsparkcrypto/lsc-byteorder32.ali
+lib/libsparkcrypto/lsc-byteorder64.ali
+lib/libsparkcrypto/lsc-byteswap32.ali
+lib/libsparkcrypto/lsc-byteswap64.ali
+lib/libsparkcrypto/lsc-debug.ali
+lib/libsparkcrypto/lsc-hmac_ripemd160.ali
+lib/libsparkcrypto/lsc-hmac_sha256.ali
+lib/libsparkcrypto/lsc-hmac_sha384.ali
+lib/libsparkcrypto/lsc-hmac_sha512.ali
+lib/libsparkcrypto/lsc-io.ali
+lib/libsparkcrypto/lsc-ops32.ali
+lib/libsparkcrypto/lsc-ops64.ali
+lib/libsparkcrypto/lsc-pad32.ali
+lib/libsparkcrypto/lsc-pad64.ali
+lib/libsparkcrypto/lsc-ripemd160-print.ali
+lib/libsparkcrypto/lsc-ripemd160.ali
+lib/libsparkcrypto/lsc-sha256-tables.ali
+lib/libsparkcrypto/lsc-sha256.ali
+lib/libsparkcrypto/lsc-sha512-tables.ali
+lib/libsparkcrypto/lsc-sha512.ali
+lib/libsparkcrypto/lsc-test.ali
+lib/libsparkcrypto/lsc-types.ali
+lib/libsparkcrypto/lsc.ali
+@dirrm include/libsparkcrypto/sharedinclude
+@dirrm include/libsparkcrypto/adainclude
+@dirrm include/libsparkcrypto
+@dirrm lib/libsparkcrypto
+@dirrmtry lib/gnat