Bug 180015

Summary: [NEW PORT] Add security/libsparkcrypto port
Product: Ports & Packages Reporter: John Marino <draco>
Component: Individual Port(s)Assignee: William Grzybowski <wg>
Status: Closed FIXED    
Severity: Affects Only Me    
Priority: Normal    
Version: Latest   
Hardware: Any   
OS: Any   
Attachments:
Description Flags
file.shar none

Description John Marino 2013-06-27 00:40:00 UTC 
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.

This port passes redports 8.4-amd64, 8.4-i386, 9.1-amd64 and 9.1-i386
It also passes pkg DEVELOPER_MODE=1.

Fix: Patch attached with submission follows:
Comment 1 William Grzybowski freebsd_committer freebsd_triage 2013-07-01 17:08:30 UTC 
Responsible Changed
From-To: freebsd-ports-bugs->wg

I'll take it.
Comment 2 John Marino 2013-07-01 17:08:31 UTC 
Redports logs:
https://redports.org/buildarchive/20130626213400-50705/
Comment 3 William Grzybowski freebsd_committer freebsd_triage 2013-07-01 17:36:15 UTC 
State Changed
From-To: open->closed

New port added. Thanks!
Comment 4 dfilter service freebsd_committer freebsd_triage 2013-07-01 17:36:24 UTC 
Author: wg
Date: Mon Jul  1 16:36:08 2013
New Revision: 322131
URL: http://svnweb.freebsd.org/changeset/ports/322131

Log:
  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>

Added:
  head/security/libsparkcrypto/
  head/security/libsparkcrypto/Makefile   (contents, props changed)
  head/security/libsparkcrypto/distinfo   (contents, props changed)
  head/security/libsparkcrypto/files/
  head/security/libsparkcrypto/files/patch-Makefile   (contents, props changed)
  head/security/libsparkcrypto/files/patch-build_libsparkcrypto.gpr   (contents, props changed)
  head/security/libsparkcrypto/pkg-descr   (contents, props changed)
  head/security/libsparkcrypto/pkg-plist   (contents, props changed)
Modified:
  head/security/Makefile

Modified: head/security/Makefile
==============================================================================
--- head/security/Makefile	Mon Jul  1 16:29:41 2013	(r322130)
+++ head/security/Makefile	Mon Jul  1 16:36:08 2013	(r322131)
@@ -282,6 +282,7 @@
     SUBDIR += libpwstor
     SUBDIR += libsectok
     SUBDIR += libsodium
+    SUBDIR += libsparkcrypto
     SUBDIR += libssh
     SUBDIR += libssh2
     SUBDIR += libtasn1

Added: head/security/libsparkcrypto/Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/security/libsparkcrypto/Makefile	Mon Jul  1 16:36:08 2013	(r322131)
@@ -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>

Added: head/security/libsparkcrypto/distinfo
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/security/libsparkcrypto/distinfo	Mon Jul  1 16:36:08 2013	(r322131)
@@ -0,0 +1,2 @@
+SHA256 (libsparkcrypto-0.1.1.tgz) = 47582d6910b8c5bb46df51d0e76c27e6fa2b13e8ab73fb4ae0f1d9f7cbd7aa6a
+SIZE (libsparkcrypto-0.1.1.tgz) = 101491

Added: head/security/libsparkcrypto/files/patch-Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/security/libsparkcrypto/files/patch-Makefile	Mon Jul  1 16:36:08 2013	(r322131)
@@ -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

Added: head/security/libsparkcrypto/files/patch-build_libsparkcrypto.gpr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/security/libsparkcrypto/files/patch-build_libsparkcrypto.gpr	Mon Jul  1 16:36:08 2013	(r322131)
@@ -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";

Added: head/security/libsparkcrypto/pkg-descr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/security/libsparkcrypto/pkg-descr	Mon Jul  1 16:36:08 2013	(r322131)
@@ -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/

Added: head/security/libsparkcrypto/pkg-plist
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/security/libsparkcrypto/pkg-plist	Mon Jul  1 16:36:08 2013	(r322131)
@@ -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
_______________________________________________
svn-ports-all@freebsd.org mailing list
http://lists.freebsd.org/mailman/listinfo/svn-ports-all
To unsubscribe, send any mail to "svn-ports-all-unsubscribe@freebsd.org"