Skip to content

matthewJamesAbbott/GlassBoxAI-CNN

BranchesTags

Repository files navigation

GlassBoxAI-CNN

Convolutional Neural Network Suite

GPU-Accelerated CNN Implementations with Formal Verification

License: MIT CUDA OpenCL Rust ONNX Kani CISA Compliant

Overview

GlassBoxAI-CNN is a comprehensive, production-ready Convolutional Neural Network implementation suite featuring:

  • Multiple GPU backends: CUDA and OpenCL acceleration
  • Multiple language implementations: C++ and Rust
  • Facade pattern architecture: Clean API separation with deep introspection capabilities
  • Formal verification: Kani-verified Rust implementation for memory safety guarantees
  • Qt GUI application: Visual training interface for the facade Rust CUDA implementation
  • CISA/NSA Secure by Design compliance: Built following government cybersecurity standards

This project demonstrates enterprise-grade software engineering practices including comprehensive testing, formal verification, cross-platform compatibility, and security-first development.

Table of Contents

  1. Features
  2. Architecture
  3. File Structure
  4. Prerequisites
  5. Installation & Compilation
  6. CLI Reference
  7. Testing
  8. Formal Verification with Kani
  9. CISA/NSA Compliance
  10. License
  11. Author

Features

Core Capabilities

Feature Description
Convolutional Layers Configurable multi-layer convolutions with custom kernel sizes
Max Pooling Spatial downsampling with configurable pool sizes
Fully Connected Layers Dense layers with arbitrary neuron counts
Training Backpropagation with Adam optimizer and gradient clipping
Activation Functions ReLU, Sigmoid, Tanh, Linear
Loss Functions MSE, Cross-Entropy with stable softmax
Model Persistence Binary and JSON serialization for model save/load
Dropout Regularization support during training
Batch Normalization Stabilize training with learnable scale/shift parameters
ONNX Export/Import Interoperability with the global AI ecosystem

GPU Acceleration

Backend Implementation Performance
CUDA Native CUDA kernels with cuRAND Optimal for NVIDIA GPUs
OpenCL Cross-platform GPU AMD, Intel, NVIDIA support

Safety & Security

Feature Technology
Memory Safety Rust ownership model
Formal Verification Kani proof harnesses (40+ proofs)
Bounds Checking Verified array access
Input Validation CLI argument validation

Architecture

┌─────────────────────────────────────────────────────────────────────┐
│                         GlassBoxAI-CNN                              │
├─────────────────────────────────────────────────────────────────────┤
│                                                                     │
│  ┌─────────────┐  ┌─────────────┐  ┌─────────────────────────────┐  │
│  │   C++ CUDA  │  │ C++ OpenCL  │  │         Rust CUDA           │  │
│  ├─────────────┤  ├─────────────┤  ├─────────────────────────────┤  │
│  │ • cnn.cu    │  │ • cnn_      │  │ • rust_cuda/                │  │
│  │ • facaded_  │  │   opencl.cpp│  │ • facaded_rust_cuda/        │  │
│  │   cnn.cu    │  │ • facaded_  │  │   ├─ kani_tests.rs          │  │
│  │             │  │   cnn_      │  │   │  (Formal Verification)  │  │
│  │             │  │   opencl.cpp│  │   └─ gui/                   │  │
│  │             │  │             │  │      (Qt GUI Application)   │  │
│  └─────────────┘  └─────────────┘  └─────────────────────────────┘  │
│                                                                     │
│  ┌─────────────────────────────────────────────────────────────────┐│
│  │                     Shared Features                             ││
│  │  • Consistent CLI interface across all implementations          ││
│  │  • Binary and JSON compatible model formats                     ││
│  │  • ONNX export/import for AI ecosystem interoperability         ││
│  │  • Batch normalization for stable training                      ││
│  │  • Comprehensive test suites                                    ││
│  └─────────────────────────────────────────────────────────────────┘│
│                                                                     │
└─────────────────────────────────────────────────────────────────────┘

File Structure

GlassBoxAI-CNN/
│
├── cnn.cu                      # C++ CUDA CNN implementation
├── cnn_opencl.cpp              # C++ OpenCL CNN implementation
├── facaded_cnn.cu              # C++ CUDA CNN with Facade pattern
├── facaded_cnn_opencl.cpp      # C++ OpenCL CNN with Facade pattern
│
├── rust_cuda/                  # Rust CUDA CNN implementation
│   ├── Cargo.toml
│   └── src/
│       ├── main.rs
│       ├── cli.rs
│       └── cnn/
│
├── facaded_rust_cuda/          # Rust CUDA CNN with Facade pattern
│   ├── Cargo.toml
│   ├── KANI_TESTS.md           # Formal verification documentation
│   ├── src/
│   │   ├── main.rs
│   │   └── kani_tests.rs       # Kani proof harnesses
│   └── gui/                    # Qt-based GUI application
│       ├── Cargo.toml
│       ├── build.rs
│       ├── qml/
│       │   └── main.qml
│       └── src/
│           ├── main.rs
│           ├── cnn.rs
│           ├── cxx_qt_bridge.rs
│           └── kani_tests.rs
│
├── cnn_cuda_tests.sh           # CUDA test suite
├── cnn_opencl_tests.sh         # OpenCL test suite
├── cnn_cpp_tests.sh            # C++ test suite
│
├── index.html                  # Project documentation
├── license.md                  # MIT License
└── README.md                   # This file

Prerequisites

Required

Dependency Version Purpose
GCC/G++ 11+ C++ compilation
CUDA Toolkit 12.0+ CUDA compilation
Rust 1.75+ Rust compilation

Optional

Dependency Version Purpose
OpenCL SDK 3.0 OpenCL compilation
Kani 0.67+ Formal verification
Qt 6 6.x GUI version

Installation & Compilation

C++ CUDA Implementation

# Standard CNN
nvcc -O2 -o cnn_cuda cnn.cu -lcurand

# Facade CNN
nvcc -O2 -o facaded_cnn_cuda facaded_cnn.cu -lcurand

C++ OpenCL Implementation

# Standard CNN
g++ -O2 -std=c++14 -o cnn_opencl cnn_opencl.cpp -lOpenCL

# Facade CNN
g++ -O2 -std=c++14 -o facaded_cnn_opencl facaded_cnn_opencl.cpp -lOpenCL

Rust CUDA Implementation

# Standard CNN
cd rust_cuda
cargo build --release

# Facade CNN
cd facaded_rust_cuda
cargo build --release

# Facade CNN with GUI
cd facaded_rust_cuda/gui
cargo build --release

Build All

# Build everything
nvcc -O2 -o cnn_cuda cnn.cu -lcurand
nvcc -O2 -o facaded_cnn_cuda facaded_cnn.cu -lcurand
g++ -O2 -std=c++14 -o cnn_opencl cnn_opencl.cpp -lOpenCL
g++ -O2 -std=c++14 -o facaded_cnn_opencl facaded_cnn_opencl.cpp -lOpenCL
(cd rust_cuda && cargo build --release)
(cd facaded_rust_cuda && cargo build --release)
(cd facaded_rust_cuda/gui && cargo build --release)

CLI Reference

Standard CNN Commands

The standard CNN implementations provide core neural network functionality.

Usage

cnn_cuda <command> [options]
cnn_opencl <command> [options]
rust_cuda/target/release/cnn_cuda <command> [options]

Commands

Command Description
create Create a new CNN model
train Train the model with data
predict Make predictions with a trained model
info Display model information
export-onnx Export model to ONNX format for interoperability
import-onnx Import model from ONNX format
help Show help message

Create Options

Option Description
--input-w=N Input width (required)
--input-h=N Input height (required)
--input-c=N Input channels (required)
--conv=N,N,... Conv filters per layer (required)
--kernels=N,N,... Kernel sizes per layer (required)
--pools=N,N,... Pool sizes per layer (required)
--fc=N,N,... FC layer sizes (required)
--output=N Output layer size (required)
--save=FILE Save model to file (required)
--lr=VALUE Learning rate (default: 0.001)
--hidden-act=TYPE sigmoid|tanh|relu|linear (default: relu)
--output-act=TYPE sigmoid|tanh|relu|linear (default: linear)
--loss=TYPE mse|crossentropy (default: mse)
--clip=VALUE Gradient clipping (default: 5.0)
--batch-norm Enable batch normalization

Train Options

Option Description
--model=FILE Load model from file (required)
--data=FILE.csv Training data CSV file (required)
--epochs=N Number of epochs (required)
--save=FILE Save trained model to file (required)
--batch-size=N Batch size (default: 32)

Predict Options

Option Description
--model=FILE Load model from file (required)
--data=FILE.csv Input data CSV file (required)
--output=FILE.csv Save predictions to CSV (required)

ONNX Export Options

Option Description
--model=FILE Load model from file (required)
--onnx=FILE ONNX output file (required)

ONNX Import Options

Option Description
--onnx=FILE ONNX input file (required)
--save=FILE Save imported model to file (required)

Examples

# Create a model for MNIST
cnn_cuda create --input-w=28 --input-h=28 --input-c=1 --conv=32,64 --kernels=3,3 --pools=2,2 --fc=128 --output=10 --save=model.bin

# Train the model
cnn_cuda train --model=model.bin --data=train.csv --epochs=50 --save=model_trained.bin

# Make predictions
cnn_cuda predict --model=model_trained.bin --data=test.csv --output=predictions.csv

# Display model info
cnn_cuda info --model=model.bin

# Create model with batch normalization
cnn_cuda create --input-w=28 --input-h=28 --input-c=1 --conv=32,64 --kernels=3,3 --pools=2,2 --fc=128 --output=10 --save=model_bn.json --batch-norm

# Export model to ONNX format
cnn_cuda export-onnx --model=model_trained.json --onnx=model.onnx

# Import model from ONNX format
cnn_cuda import-onnx --onnx=model.onnx --save=imported_model.json

Facade CNN Commands

The Facade implementations include all standard commands plus deep introspection capabilities for research and debugging.

Additional Commands

Command Description
export-onnx Export model to ONNX format for interoperability
import-onnx Import model from ONNX format
get-filter Get filter kernel weights
get-bias Get filter bias value
set-weight Set individual weight value

Facade Options

Option Description
--batch-norm Enable batch normalization (for create)
--onnx=FILE ONNX file path (for export/import-onnx)

Introspection Options

Option Description
--get-feature-map=L,F Get feature map for layer L, filter F
--get-preactivation=L,F Get pre-activation for layer L, filter F
--get-kernel=L,F Get kernel weights for layer L, filter F
--get-bias=L,F Get bias for layer L, filter F
--get-filter-gradient=L,F Get weight gradients for layer L, filter F
--get-bias-gradient=L,F Get bias gradient for layer L, filter F
--get-pooling-indices=L,F Get max pooling indices for layer L, filter F
--get-flattened Get flattened feature vector
--get-logits Get raw logits from output layer
--get-softmax Get softmax probabilities
--get-layer-stats=L Get statistics for layer L
--get-activation-hist=L Get activation histogram for layer L
--get-weight-hist=L Get weight histogram for layer L
--get-receptive-field=L Get receptive field size at layer L
--get-fc-weights=L Get fully connected weights for layer L
--get-fc-bias=L Get fully connected bias for layer L
--get-dropout-mask=L Get dropout mask for layer L
--add-filter=L,N Add N new filters to layer L
--get-num-filters=L Get number of filters in layer L
--set-bias=L,F,V Set bias for layer L, filter F to value V
--set-fc-bias=L,N,V Set FC bias for layer L, neuron N to value V

Facade Examples

# Create a new model
facaded_cnn_cuda create --input-w=28 --input-h=28 --input-c=1 --conv=32,64 --kernels=3,3 --pools=2,2 --fc=128 --output=10 --save=model.bin

# Create model with batch normalization
facaded_cnn_cuda create --input-w=28 --input-h=28 --input-c=1 --conv=32,64 --kernels=3,3 --pools=2,2 --fc=128 --output=10 --save=model_bn.json --batch-norm

# Get model information
facaded_cnn_cuda info --model=model.bin

# Inspect filter weights
facaded_cnn_cuda get-filter --model=model.bin --layer=0 --filter=0 --channel=0

# Get feature map after forward pass
facaded_cnn_cuda --get-feature-map=0,0 --model=model.bin

# Get layer statistics
facaded_cnn_cuda --get-layer-stats=0 --model=model.bin

# Get softmax probabilities
facaded_cnn_cuda --get-softmax --model=model.bin

# Export model to ONNX format
facaded_cnn_cuda export-onnx --model=model.json --onnx=model.onnx

# Import model from ONNX format
facaded_cnn_cuda import-onnx --onnx=model.onnx --save=imported_model.json

Testing

Running All Tests

# Run CUDA tests
./cnn_cuda_tests.sh

# Run OpenCL tests
./cnn_opencl_tests.sh

# Run C++ tests
./cnn_cpp_tests.sh

# Run Rust tests
cd rust_cuda && cargo test
cd facaded_rust_cuda && cargo test

Test Categories

Each test suite covers:

Category Tests
Help & Usage Command-line interface verification
Model Creation Various architecture configurations
Hyperparameters Learning rate, activation, loss functions
Model Info Metadata retrieval
Save & Load Model persistence
Introspection Filter, bias, feature map inspection
Error Handling Invalid input handling
Cross-Implementation API compatibility
Train & Predict End-to-end workflows

Test Output Example

=========================================
CNN CUDA Comprehensive Test Suite
=========================================

Group: Help & Usage
Test 1: CNN help command... PASS
Test 2: CNN --help flag... PASS
Test 3: CNN -h flag... PASS
...

=========================================
Test Summary
=========================================
Total tests: 50
Passed: 50
Failed: 0

All tests passed!

Formal Verification with Kani

Overview

The Rust Facade implementation includes Kani formal verification proofs that mathematically prove the absence of certain classes of bugs. This goes beyond traditional testing to provide mathematical guarantees about code correctness.

Verification Categories

The test suite covers 15 security verification categories:

Category Description
Strict Bound Checks Array/collection indexing safety
Pointer Validity Slice-to-pointer conversion safety
No-Panic Guarantee Enum and command handling safety
Integer Overflow Prevention Weight size, dimension calculations
Division-by-Zero Exclusion Launch config, pooling stride
Global State Consistency Training mode state tracking
Deadlock-Free Logic Arc reference counting
Input Sanitization Bounds Loop iteration limits
Result Coverage Audit Error handling completeness
Memory Leak Prevention Vector allocation bounds
Constant-Time Execution Timing-safe operations
State Machine Integrity Training state transitions
Enum Exhaustion Match statement completeness
Floating-Point Sanity NaN/Infinity prevention
Resource Limit Compliance Memory budget enforcement

Key Kani Proofs

Bound Checking Proofs

  • verify_conv_filter_indexing ✓
  • verify_output_indexing ✓
  • verify_parse_args_bounds ✓

Overflow Prevention Proofs

  • verify_weight_size_no_overflow ✓
  • verify_output_dimension_no_overflow ✓
  • verify_adam_timestep_no_overflow ✓

Safety Proofs

  • verify_activation_type_no_panic ✓
  • verify_loss_type_no_panic ✓
  • verify_command_parsing_no_panic ✓
  • verify_relu_no_nan ✓
  • verify_gradient_clipping ✓

Running Kani Verification

# CLI Version
cd facaded_rust_cuda
cargo kani

# GUI Version
cd facaded_rust_cuda/gui
cargo kani

# Run specific proof
cargo kani --harness verify_conv_filter_indexing

Why Formal Verification Matters

Traditional testing can only verify specific test cases. Formal verification with Kani:

  • Exhaustively checks all possible inputs within defined bounds
  • Mathematically proves absence of panics, buffer overflows, and undefined behavior
  • Catches edge cases that random testing might miss
  • Provides cryptographic-level assurance for safety-critical code

CISA/NSA Compliance

Secure by Design

This project follows CISA (Cybersecurity and Infrastructure Security Agency) and NSA (National Security Agency) Secure by Design principles:

Principle Implementation
Memory Safety Rust ownership model eliminates buffer overflows, use-after-free, and data races
Formal Verification Kani proofs mathematically verify absence of critical bugs
Input Validation All CLI inputs validated before processing
Defense in Depth Multiple layers of safety (language, compiler, runtime checks)
Secure Defaults Safe default configurations throughout
Transparency Open source with full code visibility

Compliance Checklist

  • Memory-safe language (Rust implementation)
  • Static analysis (Rust compiler + Clippy)
  • Formal verification (Kani proof harnesses)
  • Comprehensive testing (Unit tests + integration tests)
  • Bounds checking (Verified array access)
  • Input validation (CLI argument parsing)
  • No unsafe code in critical paths (Where possible)
  • Documentation (Inline docs + README)
  • Version control (Git)
  • License clarity (MIT License)

Attestation

This codebase has been developed following secure software development lifecycle (SSDLC) practices and demonstrates:

  • 40+ formal verification proofs passed (Kani proofs across CLI and GUI)
  • Zero warnings compilation across all implementations
  • Consistent API across all language/backend combinations
  • Production-ready code quality

License

MIT License

Copyright (c) 2025 Matthew Abbott

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

Author

Matthew Abbott
Email: mattbachg@gmail.com

Built with precision. Verified with rigor. Secured by design.

About

No description, website, or topics provided.

Resources

Readme

License

MIT license
Activity

Stars

0 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

 
 
 

Contributors

Languages