SECURE SOFTWARE SOURCE CODE VERIFICATION TOOLS

THE NATURE OF THE BUILT-IN FLEXIBILITY OF A COMPUTER SYSTEM MAKES IT EXTREMELY VULNERABLE TO BOTH THE NEGLIGENCE OF AUTHORIZED USERS AND INTENTIONAL, SURREPTITIOUS ATTACKS BY ADVERSARIES. SECURE SOFTWARE IS THE USER'S GOAL. SECURE SOFTWARE IS SOFTWARE WHICH ADHERES TO THE CRITERIA DICTATED BY THE ORANGE BOOK (CSC-STD-001-83). IT CAN BE TRUSTED TO CORRESPOND EXACTLY TO ITS DESIGN SPECIFICATIONS. ALSO, IT OUGHT NOT DEVIATE FROM THAT DESIGN AFTER ENTERING THE IMPLEMENTATION PHASE. SECURE SOFTWARE DESIGN IS CURRENTLY FEASIBLE THROUGH STATEOF-THE-ART DESIGN VERIFICATION. HOWEVER, CODE VERIFICATION IS LARGELY A MANUAL ART, HIGHLY DEPENDENT ON THE SKILL AND EXPERTISE OF THE RESEARCHER. COMPUSEC PROPOSES A REVOLUTIONARY AUTOMATED CONCEPT WHEREIN IMPLEMENTED CODE CAN BE DIRECTLY VERIFIED FOR ADHERANCE TO SPECIFICATION. THUS THE GAP BETWEEN DESIGN AND IMPLEMENTATION IS CLOSED. BACKDOORS, TRAPDOORS AND TIMEBOMBS (IF INSERTED IN THE TIMEFRAME BETWEEN DESIGN AND IMPLEMENTATION) WILL HENCEFORTH BE DETECTABLE BY VERIFICATION OF THE ACTUALLY IMPLEMENTED CODE.