Bug 180015 - [NEW PORT] Add security/libsparkcrypto port
Summary: [NEW PORT] Add security/libsparkcrypto port
Status: Closed FIXED
Alias: None
Product: Ports & Packages
Classification: Unclassified
Component: Individual Port(s) (show other bugs)
Version: Latest
Hardware: Any Any
: Normal Affects Only Me
Assignee: William Grzybowski
URL:
Keywords:
Depends on:
Blocks:
 
Reported: 2013-06-27 00:40 UTC by John Marino
Modified: 2013-07-01 17:40 UTC (History)
0 users

See Also:


Attachments
file.shar (10.44 KB, text/plain)
2013-06-27 00:40 UTC, John Marino
no flags Details

Note You need to log in before you can comment on or make changes to this bug.
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 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 2013-07-01 17:36:15 UTC
State Changed
From-To: open->closed

New port added. Thanks!
Comment 4 dfilter service freebsd_committer 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"