src/luks_struct.h: move struct from src/luks.h to this new file

src/Makefile.am

@@ -42,7 +42,7 @@ base_C			= $(smallbase_C) autoset.c ewf.c fnctdsk.c hdaccess.c hdcache.c hdwin32
 base_H			= $(smallbase_H) alignio.h autoset.h ewf.h fnctdsk.h hdaccess.h hdwin32.h hidden.h guid_cmp.h guid_cpy.h hdcache.h hpa_dco.h intrf.h iso.h iso9660.h lang.h list.h list_sort.h log_part.h types.h io_redir.h msdos.h ntfs_utl.h parti386.h partgpt.h parthumax.h partmac.h partsun.h partxbox.h partauto.h sudo.h unicode.h win32.h
 
 fs_C			= analyse.c bfs.c bsd.c btrfs.c cramfs.c exfat.c ext2.c fat.c fatx.c f2fs.c jfs.c gfs2.c hfs.c hfsp.c hpfs.c luks.c lvm.c md.c netware.c ntfs.c refs.c rfs.c savehdr.c sun.c swap.c sysv.c ufs.c vmfs.c wbfs.c xfs.c zfs.c
-fs_H			= analyse.h bfs.h bsd.h btrfs.h cramfs.h exfat.h ext2.h fat.h fatx.h f2fs.h f2fs_fs.h jfs_superblock.h jfs.h gfs2.h hfs.h hfsp.h hpfs.h hfsp_struct.h luks.h lvm.h md.h netware.h ntfs.h ntfs_struct.h refs.h rfs.h savehdr.h sun.h swap.h sysv.h ufs.h vmfs.h wbfs.h xfs.h zfs.h
+fs_H			= analyse.h bfs.h bsd.h btrfs.h cramfs.h exfat.h ext2.h fat.h fatx.h f2fs.h f2fs_fs.h jfs_superblock.h jfs.h gfs2.h hfs.h hfsp.h hpfs.h hfsp_struct.h luks.h luks_struct.h lvm.h md.h netware.h ntfs.h ntfs_struct.h refs.h rfs.h savehdr.h sun.h swap.h sysv.h ufs.h vmfs.h wbfs.h xfs.h zfs.h
 
 testdisk_ncurses_C	= addpart.c addpartn.c adv.c askloc.c chgarch.c chgarchn.c chgtype.c chgtypen.c dimage.c dirn.c dirpart.c diskacc.c diskcapa.c edit.c ext2_sb.c ext2_sbn.c fat1x.c fat32.c fat_adv.c fat_cluster.c fatn.c geometry.c geometryn.c godmode.c hiddenn.c intrface.c intrfn.c nodisk.c ntfs_adv.c ntfs_fix.c ntfs_udl.c parti386n.c partgptn.c partmacn.c partsunn.c partxboxn.c tanalyse.c tbanner.c tdelete.c tdiskop.c tdisksel.c testdisk.c texfat.c thfs.c tload.c tlog.c tmbrcode.c tntfs.c toptions.c tpartwr.c 
 testdisk_ncurses_H	= addpart.h addpartn.h adv.h askloc.h chgarch.h chgarchn.h chgtype.h chgtypen.h dimage.h dirn.h dirpart.h diskacc.h diskcapa.h edit.h ext2_sb.h ext2_sbn.h fat1x.h fat32.h fat_adv.h fat_cluster.h fatn.h geometry.h geometryn.h godmode.h hiddenn.h intrface.h intrfn.h nodisk.h ntfs_adv.h ntfs_fix.h ntfs_udl.h partgptn.h parti386n.h partmacn.h partsunn.h partxboxn.h tanalyse.h tdelete.h tdiskop.h tdisksel.h texfat.h thfs.h tload.h tlog.h tmbrcode.h tntfs.h toptions.h tpartwr.h
@@ -389,7 +389,7 @@ file_C			= filegen.c \
 			  file_zip.c \
 			  file_zpr.c
 
-file_H			= ext2.h hfsp_struct.h filegen.h file_doc.h file_jpg.h file_gz.h file_sp3.h file_tar.h file_tiff.h file_txt.h ntfs_struct.h ole.h pe.h suspend.h
+file_H			= ext2.h hfsp_struct.h filegen.h file_doc.h file_jpg.h file_gz.h file_sp3.h file_tar.h file_tiff.h file_txt.h luks_struct.h ntfs_struct.h ole.h pe.h suspend.h
 
 photorec_C		= photorec.c phcfg.c addpart.c chgarch.c chgtype.c dir.c exfatp.c ext2grp.c ext2_dir.c ext2p.c fat_dir.c fatp.c file_found.c geometry.c ntfs_dir.c ntfsp.c pdisksel.c poptions.c sessionp.c dfxml.c partgptro.c
 

src/file_luks.c

@@ -32,8 +32,9 @@
 #include "types.h"
 #include "filegen.h"
 #include "common.h"
-#include "luks.h"
+#include "luks_struct.h"
 
+/*@ requires \valid(file_stat); */
 static void register_header_check_luks(file_stat_t *file_stat);
 
 const file_hint_t file_hint_luks= {
@@ -45,14 +46,22 @@ const file_hint_t file_hint_luks= {
   .register_header_check=&register_header_check_luks
 };
 
-static const unsigned char luks_header[6]=  {
+/*@
-  'L' , 'U' , 'K' , 'S' , 0xba, 0xbe
+  @ requires buffer_size >= sizeof(struct luks_phdr);
-};
+  @ requires \valid_read(buffer+(0..buffer_size-1));
-
+  @ requires valid_file_recovery(file_recovery);
+  @ requires \valid(file_recovery_new);
+  @ requires file_recovery_new->blocksize > 0;
+  @ requires separation: \separated(&file_hint_luks, buffer+(..), file_recovery, file_recovery_new);
+  @ ensures  \result == 0 || \result == 1;
+  @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
+  @*/
 static int header_check_luks(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
 {
   const struct luks_phdr *hdr=(const struct luks_phdr *)buffer;
-  if(be16(hdr->version)<1 || be16(hdr->version)>2)
+  const unsigned int version=be16(hdr->version);
+  if(version<1 || version>2)
     return 0;
   if(!isalpha(hdr->cipherName[0]))
     return 0;
@@ -64,6 +73,9 @@ static int header_check_luks(const unsigned char *buffer, const unsigned int buf
 
 static void register_header_check_luks(file_stat_t *file_stat)
 {
+  static const unsigned char luks_header[6]=  {
+    'L' , 'U' , 'K' , 'S' , 0xba, 0xbe
+  };
   register_header_check(0, luks_header, sizeof(luks_header), &header_check_luks, file_stat);
 }
 #endif

src/luks.h

@@ -22,43 +22,26 @@
  */
 #ifndef _LUKS_H
 #define _LUKS_H
+#include "luks_struct.h"
 #ifdef __cplusplus
 extern "C" {
 #endif
 
-#define LUKS_CIPHERNAME_L	32
+/*@
-#define LUKS_CIPHERMODE_L	32
+  @ requires \valid(disk_car);
-#define LUKS_HASHSPEC_L		32
+  @ requires valid_disk(disk_car);
-#define LUKS_DIGESTSIZE		20
+  @ requires \valid(partition);
-#define LUKS_SALTSIZE		32
+  @ requires \separated(disk_car, partition);
-#define LUKS_NUMKEYS		8
+  @*/
-#define LUKS_MAGIC_L 		6
-#define UUID_STRING_L 		40
-typedef struct luks_keyslot luks_keyslot_t;
-struct luks_keyslot {
-  uint32_t	active;
-  uint32_t	passwordIterations;
-  uint8_t	passwordSalt[LUKS_SALTSIZE];
-  uint32_t	keyMaterialOffset;
-  uint32_t	stripes;
-};
-
-struct luks_phdr {
-  uint8_t	magic[LUKS_MAGIC_L];
-  uint16_t	version;
-  uint8_t	cipherName[LUKS_CIPHERNAME_L];
-  uint8_t	cipherMode[LUKS_CIPHERMODE_L];
-  uint8_t	hashSpec[LUKS_HASHSPEC_L];
-  uint32_t	payloadOffset;
-  uint32_t	keyBytes;
-  uint8_t	mkDigest[LUKS_DIGESTSIZE];
-  uint8_t	mkDigestSalt[LUKS_SALTSIZE];
-  uint32_t	mkDigestIterations;
-  uint8_t	uuid[UUID_STRING_L];
-  luks_keyslot_t keyslot[LUKS_NUMKEYS];
-};
-
 int check_LUKS(disk_t *disk_car, partition_t *partition);
+
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(sb);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, sb, partition);
+  @*/
 int recover_LUKS(const disk_t *disk_car, const struct luks_phdr *sb, partition_t *partition, const int verbose, const int dump_ind);
 
 #ifdef __cplusplus

src/luks_struct.h

@@ -0,0 +1,65 @@
+/*
+
+    File: luks_struct.h
+
+    Copyright (C) 2007 Christophe GRENIER <grenier@cgsecurity.org>
+
+    This software is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write the Free Software Foundation, Inc., 51
+    Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+    LUKS on-disk-format: http://luks.endorphin.org/spec
+ */
+#ifndef _LUKS_STRUCT_H
+#define _LUKS_STRUCT_H
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#define LUKS_CIPHERNAME_L	32
+#define LUKS_CIPHERMODE_L	32
+#define LUKS_HASHSPEC_L		32
+#define LUKS_DIGESTSIZE		20
+#define LUKS_SALTSIZE		32
+#define LUKS_NUMKEYS		8
+#define LUKS_MAGIC_L 		6
+#define UUID_STRING_L 		40
+typedef struct luks_keyslot luks_keyslot_t;
+struct luks_keyslot {
+  uint32_t	active;
+  uint32_t	passwordIterations;
+  uint8_t	passwordSalt[LUKS_SALTSIZE];
+  uint32_t	keyMaterialOffset;
+  uint32_t	stripes;
+};
+
+struct luks_phdr {
+  uint8_t	magic[LUKS_MAGIC_L];
+  uint16_t	version;
+  uint8_t	cipherName[LUKS_CIPHERNAME_L];
+  uint8_t	cipherMode[LUKS_CIPHERMODE_L];
+  uint8_t	hashSpec[LUKS_HASHSPEC_L];
+  uint32_t	payloadOffset;
+  uint32_t	keyBytes;
+  uint8_t	mkDigest[LUKS_DIGESTSIZE];
+  uint8_t	mkDigestSalt[LUKS_SALTSIZE];
+  uint32_t	mkDigestIterations;
+  uint8_t	uuid[UUID_STRING_L];
+  luks_keyslot_t keyslot[LUKS_NUMKEYS];
+};
+
+#ifdef __cplusplus
+} /* closing brace for extern "C" */
+#endif
+#endif
+