Merge pull request #27 from DavisPL/main

dataset/cwe-dafny/CWE-22/path-traversal-wtih-open.dfy

@@ -0,0 +1,34 @@
+include "../../../filesystems-api/interface/effectful-interface.dfy"
+method GetFile(filename: seq<char>) returns (data: array<byte>)
+// requires non_empty_string(filename)
+// requires !has_dangerous_pattern(filename)
+// requires is_valid_file_name(filename)
+// requires has_valid_file_length(filename)
+// requires is_valid_file_extension(filename)
+{
+
+    var f: FileStream;
+    var ok: bool;
+    var base_dir: seq<char> := "/var/www/files/";
+    data := new byte[100];
+    var file_path := Join(base_dir, filename);
+    // if (!has_dangerous_pattern(file_path)) {
+        print "base_dir is safe";
+        ok, f := FileStream.Open(file_path);
+
+        // if !ok { print "open failed"; return data; }
+        // // if is_valid_file_extension(file_path) {
+        //     print "file extension is valid";
+        //     ok := f.Read(file_path, 0, data, 0, data.Length as int32);
+        //     print "Read operation terminated safely";
+    //     } else {
+    //         print "file extension is invalid";
+    //         return data;
+    //     }
+
+    // }  else {
+    //         print "base_dir is unsafe";
+    //         return data;
+    // }
+
+}

dataset/cwe-dafny/methods.txt

@@ -0,0 +1,3 @@
+1. add preconditions to JoinFileToPath
+2. use if (...) checks to guard the function call to FileStream.Open
+3. use expect (...) checks to add runtime checks that the preconditions hold

dataset/cwe-python/task_id_1_with_expect.dfy → dataset/cwe-dafny/task_id_1_with_expect.dfy

@@ -1,4 +1,4 @@
-include "/Users/pari/pcc-llms/dataset/filesystems/interface/effectful-interface.dfy"
+include "../../filesystems-api/interface/effectful-interface.dfy"
 
 
 method JoinFileToPath(path: seq<char>,  fname: seq<char>) returns (jointPath: path)

dataset/cwe-python/CWE-378/cwe-378.py

@@ -4,7 +4,7 @@
 
 def process_sensitive_data(data):
     # Create a temporary file with default permissions
-    temp_file = tempfile.NamedTemporaryFile(mode='w+t', delete=False)
+    temp_file = tempfile.NamedTemporaryFile(mode='w+t', delete=False) # Add a temp txt file
     temp_file.write(data)
     temp_file.close()
 
@@ -21,6 +21,7 @@ def process_sensitive_data(data):
 sensitive_info = "password123"
 result = process_sensitive_data(sensitive_info)
 
+#TODO separate the safe code from the unsafe code and task description and add safe dafny version and a code completion sample in Dafny
 # A program that creates a temporary file to store sensitive data 
 # The temporary file is created with default permissions, which might be 
 # too permissive and allow other users on the system to read the sensitive data

dataset/cwe-python/CWE-59/scenario2/task-description.txt

@@ -0,0 +1,5 @@
+File retrieval and file upload for a username
+
+1. Take a username as input
+2. Construct a path to a file named "user_data.txt" in the user's home directory
+3. If the file exists, read and return its contents

dataset/test/passwd.txt

@@ -0,0 +1 @@
+uehfyJHD$73@0!j.Lz

filesystems-api/interface/effectful-interface.dfy

@@ -119,8 +119,6 @@ class FileStream
       requires has_absoloute_path(p)
       requires is_valid_file_extension(p)
       requires has_valid_content_length(buffer)     
-      requires is_valid_file_extension(p)
-      requires is_valid_file_extension(p)
       requires IsOpen()
       requires 0 <= start as int <= end as int <= buffer.Length
       modifies buffer

output/task_id_6/task_id_6-gpt-4-temp_0.0-k_1.dfy → output/task_id_6_generated@2024-09-18-01-14/task_id_6-gpt-4-temp_0.75-k_1.dfy

@@ -1,6 +1,7 @@
-include "/Users/pari/pcc-llms/dataset/filesystems/interface/effectful-interface.dfy"
+include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy"
 
 method CreateFullPath(filename: seq<char>) returns (fullPath: seq<char>)
+ requires non_empty_string(filename)
  requires !has_dangerous_pattern(filename)
  requires is_valid_file_name(filename)
  requires has_valid_file_length(filename)

output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy

@@ -0,0 +1,17 @@
+include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy"
+
+method GetFile(filename: seq<char>) returns (data: array<byte>)
+ requires non_empty_string(filename)
+ requires !has_dangerous_pattern(filename)
+ requires is_valid_file_name(filename)
+ requires has_valid_file_length(filename)
+ {
+     var directory: seq<char> := "/var/www/files/";
+     var f: FileStream;
+     var fullpath := Join(directory, filename);
+     var ok: bool;
+     ok, f := Open(fullpath);
+     if !ok { print "open failed"; return new byte[0]; }
+     data := new byte[100];
+     ok := f.Read(fullpath, 0, data, 0, data.Length as int32);
+ }

output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1_verification_log.txt

@@ -0,0 +1,11 @@
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy(13,14): Error: unresolved identifier: Open
+   |
+13 |      ok, f := Open(fullpath);
+   |               ^^^^
+
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_1.dfy(13,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment
+   |
+13 |      ok, f := Open(fullpath);
+   |            ^^
+
+2 resolution/type errors detected in task_id_7-gpt-4-temp_0.75-k_1.dfy

output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy

@@ -0,0 +1,20 @@
+include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy"
+
+method GetFile(filename: seq<char>) returns (data: array<byte>)
+ requires !has_dangerous_pattern(filename)
+ requires is_valid_file_extension(filename)
+ requires is_valid_file_name(filename)
+ requires has_valid_file_length(filename)
+ requires has_absoloute_path(filename)
+ requires non_empty_string(filename)
+ {
+     var f: FileStream;
+     var ok: bool;
+     var path: array<char> := "/var/www/files/";
+     var fullPath := Join(path, filename);
+     ok, f := FileStream.Open(fullPath);
+     if !ok { print "open failed"; return new byte[0]; }
+     data := new byte[100];
+     ok := f.Read(fullPath, 0, data, 0, data.Length as int32);
+     print "File read completed!\n";
+ }

output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2_verification_log.txt

@@ -0,0 +1,11 @@
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy(13,27): Error: RHS (of type string) not assignable to LHS (of type array<char>)
+   |
+13 |      var path: array<char> := "/var/www/files/";
+   |                            ^^
+
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_2.dfy(14,21): Error: incorrect argument type at index 0 for method in-parameter 'p' (expected path, found array<char>)
+   |
+14 |      var fullPath := Join(path, filename);
+   |                      ^^^^^^^^^^^^^^^^^^^^
+
+2 resolution/type errors detected in task_id_7-gpt-4-temp_0.75-k_2.dfy

output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy

@@ -0,0 +1,18 @@
+include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy"
+
+method GetFile(filename: seq<char>) returns (data: array<byte>)
+ requires !has_dangerous_pattern(filename)
+ requires is_valid_file_name(filename)
+ requires non_empty_string(filename)
+ requires has_valid_file_length(filename)
+ {
+    var folderPath: seq<char> := "/var/www/files/";
+    var fullPath: seq<char> := Join(folderPath, filename);
+    var f: FileStream;
+    var ok: bool;
+    ok, f := FileStream.Open(fullPath);
+    if !ok { print "open failed\n"; return new byte[0]; }
+    data := new byte[100];
+    ok := f.Read(fullPath, 0, data, 0, data.Length as int32);
+    print "File data loaded!\n";
+ }

output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3_verification_log.txt

@@ -0,0 +1,42 @@
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy(13,4): Error: a precondition for this call could not be proved
+   |
+13 |     ok, f := FileStream.Open(fullPath);
+   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(104,13): Related location: this is the precondition that could not be proved
+    |
+104 |     requires !has_dangerous_pattern(name)
+    |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy(16,4): Error: a precondition for this call could not be proved
+   |
+16 |     ok := f.Read(fullPath, 0, data, 0, data.Length as int32);
+   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved
+    |
+120 |       requires is_valid_file_extension(p)
+    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(211,4): Related location: this proposition could not be proved
+    |
+211 |     lastDotIndex >= 0 &&
+    |     ^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_3.dfy(16,4): Error: a precondition for this call could not be proved
+   |
+16 |     ok := f.Read(fullPath, 0, data, 0, data.Length as int32);
+   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved
+    |
+120 |       requires is_valid_file_extension(p)
+    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(212,4): Related location: this proposition could not be proved
+    |
+212 |     lastDotIndex < |filename| - 1 &&
+    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+
+Dafny program verifier finished with 0 verified, 3 errors

output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy

@@ -0,0 +1,18 @@
+include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy"
+
+method GetFile(filename: seq<char>) returns (data: array<byte>)
+ requires !has_dangerous_pattern(filename)
+ requires is_valid_file_name(filename)
+ requires non_empty_string(filename)
+ requires has_valid_file_length(filename)
+ {
+   var f: FileStream;
+   var ok: bool;
+   var dir: path := "/var/www/files/"; 
+   var fullpath: path := Join(dir, filename);
+   ok, f := FileStream.Open(fullpath);
+   if !ok { print "open failed\n"; return new byte[0]; }
+   data := new byte[100];
+   ok := f.Read(fullpath, 0, data, 0, data.Length as int32);
+   print "File data loaded!\n";
+ }

output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4_verification_log.txt

@@ -0,0 +1,42 @@
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy(13,3): Error: a precondition for this call could not be proved
+   |
+13 |    ok, f := FileStream.Open(fullpath);
+   |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(104,13): Related location: this is the precondition that could not be proved
+    |
+104 |     requires !has_dangerous_pattern(name)
+    |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy(16,3): Error: a precondition for this call could not be proved
+   |
+16 |    ok := f.Read(fullpath, 0, data, 0, data.Length as int32);
+   |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved
+    |
+120 |       requires is_valid_file_extension(p)
+    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(211,4): Related location: this proposition could not be proved
+    |
+211 |     lastDotIndex >= 0 &&
+    |     ^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_4.dfy(16,3): Error: a precondition for this call could not be proved
+   |
+16 |    ok := f.Read(fullpath, 0, data, 0, data.Length as int32);
+   |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved
+    |
+120 |       requires is_valid_file_extension(p)
+    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(212,4): Related location: this proposition could not be proved
+    |
+212 |     lastDotIndex < |filename| - 1 &&
+    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+
+Dafny program verifier finished with 0 verified, 3 errors

output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy

@@ -0,0 +1,18 @@
+include "/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy"
+
+method GetFile(filename: seq<char>) returns (data: array<byte>)
+ requires non_empty_string(filename)
+ requires !has_dangerous_pattern(filename)
+ requires is_valid_file_name(filename)
+ requires has_valid_file_length(filename)
+ {
+     var ok: bool;
+     var f: FileStream;
+     var directory: path := "/var/www/files/";
+     var fullPath := Join(directory, filename);
+     ok, f := FileStream.Open(fullPath);
+     if !ok { print "open failed"; return new byte[0]; }
+     data := new byte[100];
+     ok := f.Read(fullPath, 0, data, 0, data.Length as int32);
+     print "File data loaded!\n";
+ }

output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5_verification_log.txt

@@ -0,0 +1,42 @@
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy(13,5): Error: a precondition for this call could not be proved
+   |
+13 |      ok, f := FileStream.Open(fullPath);
+   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(104,13): Related location: this is the precondition that could not be proved
+    |
+104 |     requires !has_dangerous_pattern(name)
+    |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy(16,5): Error: a precondition for this call could not be proved
+   |
+16 |      ok := f.Read(fullPath, 0, data, 0, data.Length as int32);
+   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved
+    |
+120 |       requires is_valid_file_extension(p)
+    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(211,4): Related location: this proposition could not be proved
+    |
+211 |     lastDotIndex >= 0 &&
+    |     ^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/output/task_id_7_generated@2024-09-18-09-16/task_id_7-gpt-4-temp_0.75-k_5.dfy(16,5): Error: a precondition for this call could not be proved
+   |
+16 |      ok := f.Read(fullPath, 0, data, 0, data.Length as int32);
+   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/effectful-interface.dfy(120,15): Related location: this is the precondition that could not be proved
+    |
+120 |       requires is_valid_file_extension(p)
+    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+/Users/pari/pcc-llms/filesystems-api/interface/interface-helper.dfy(212,4): Related location: this proposition could not be proved
+    |
+212 |     lastDotIndex < |filename| - 1 &&
+    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+
+Dafny program verifier finished with 0 verified, 3 errors